# 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

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]
``````
3 Likes

Awesome, thanks a lot!