Hi everyone!
How does one resolve the following type variable ambiguities for non-injective type families?
The minimal example below:
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, AllowAmbiguousTypes #-}
import Data.Singletons
import Data.Singletons.Prelude
type family NList ns b where
NList '[] b = ()
NList (_ ': xs) b = [NList xs b]
y :: SList ns -> NList ns a
y SNil = ()
y (SCons _x xs) = [y xs]
Provides the following error message:
minimal-example.hs:12:19: error:
β’ Could not deduce: NList n2 a ~ NList n2 a0
from the context: ns ~ (n1 : n2)
bound by a pattern with constructor:
SCons :: forall a (n1 :: a) (n2 :: [a]).
Sing n1 -> Sing n2 -> SList (n1 : n2),
in an equation for βyβ
at minimal-example.hs:12:4-14
Expected type: NList ns a
Actual type: [NList n2 a0]
NB: βNListβ is a non-injective type family
The type variable βa0β is ambiguous
β’ In the expression: [y xs]
In an equation for βyβ: y (SCons _x xs) = [y xs]
β’ Relevant bindings include
xs :: Sing n2 (bound at minimal-example.hs:12:13)
y :: SList ns -> NList ns a (bound at minimal-example.hs:11:1)
|
12 | y (SCons _x xs) = [y xs]
| ^^^^^^
I have tried using TypeApplications
with [y @a xs]
but it says type variable a
is not in scope, and I am not sure how to bring it in scope