Handling type variable ambiguities with non-injective type families?

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 :expressionless:

You can use ScopedTypeVariables for that.

{-# LANGUAGE TypeApplications, ScopedTypeVariables #-}
y :: forall ns a. SList ns -> NList ns a
y SNil = ()
y (SCons _x xs) = [y @_ @a xs]

Awesome, thanks a lot! :smile: