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 
