Ambiguity error with higher order lists and type families

Question

I have a higher order list GADT defined like so:

data HList as where
    HNil :: HList '[]
    HCons :: a -> HList as -> HList (a ': as)

I can write a function that gets me the first item from that list, provided it is non-empty:

first :: HList (a ': as) -> HList '[a]
first (HCons a _) = HCons a HNil

However, if I make a new type Cat and a type family that merely applies every type in a type-level list to Cat (kind of like a type level map):

newtype Cat a = Cat a

type family MapCat (as :: [*]) :: [*] where
    MapCat '[] = '[]
    MapCat (a ': as) = Cat a ': MapCat as

And a type CatList which converts a list of types to a HList full of those types applied to Cat:

type CatList cs = HList (MapCat cs)

I can't write a similar function that works on CatList.

first' :: CatList (a ': as) -> CatList '[a]
first' (HCons a _) = HCons a HNil

It errors out with:

Couldn't match type ‘MapCat as0’ with ‘MapCat as’
NB: ‘MapCat’ is a type function, and may not be injective
The type variable ‘as0’ is ambiguous
Expected type: CatList (a : as) -> CatList '[a]
  Actual type: CatList (a : as0) -> CatList '[a]
In the ambiguity check for:
  forall a (as :: [*]). CatList (a : as) -> CatList '[a]
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
  Testing.fst :: CatList (a : as) -> CatList '[a]

What's going wrong? Here is a gist with the entire code.

Answer 1

Let's start with a simpler example:

type family F a

err :: F a -> ()
err _ = ()

throws

Couldn't match type ‘F a0’ with ‘F a’ NB:
F is a type function, and may not be injective
The type variable a0 is ambiguous
Expected type: F a -> ()
  Actual type: F a0 -> () …

While this compiles fine:

ok :: (a ~ Int) => F a -> ()
ok _ = ()

And this:

type family F a where
    F a = a

ok :: F a -> ()
ok _ = ()

Here is another example, that closer to your problem:

data D = C

data Id (d :: D) where
    Id :: Id d

type family TF_Id (d :: D) :: D where
    TF_Id C = C

err :: Id (TF_Id d) -> ()
err _ = ()

The error is

Couldn't match type ‘TF_Id d0’ with ‘TF_Id d’ NB:
TF_Id is a type function, and may not be injective
The type variable d0 is ambiguous
Expected type: Id (TF_Id d) -> ()
  Actual type: Id (TF_Id d0) -> () …

But this works:

ok :: Id (TF_Id C) -> ()
ok _ = ()

and this:

type family TF_Id (d :: D) :: D where
    TF_Id x = x

ok :: Id (TF_Id d) -> ()
ok _ = ()

since TF_Id a immediately reduces to a in both cases.

So the compiler throws an error every time it cannot reduce SomeTypeFamily a, where a is some type variable, that was not determined previously.

So if we want to fix this:

type family TF_Id (d :: D) :: D where
    TF_Id C = C

err :: Id (TF_Id d) -> ()
err _ = ()

without redefining the type family, we need to determine d in the err type signature. The simplest way is

type family TF_Id (d :: D) :: D where
    TF_Id C = C

ok :: Id d -> Id (TF_Id d) -> ()
ok _ _ = ()

Or we can define a datatype for this:

data Proxy (d :: D) = Proxy

ok :: Proxy d -> Id (TF_Id d) -> ()
ok _ _ = ()

And now back to the first' function:

data Proxy (a :: [*]) = Proxy

first' :: Proxy (a ': as) -> CatList (a ': as) -> CatList '[a]
first' _ (HCons a _) = HCons a HNil

This compiles fine. You can use it like this:

main = print $ first' (Proxy :: Proxy '[Int, Bool]) (HCons (Cat 3) $ HCons (Cat True) HNil)

which prints Cat3:[].

But the only thing the compiler must know to reduce MapCat as is a weak head normal form of as, so we do not actually need to provide this additional type information in Proxy :: Proxy '[Int, Bool]. Here is a better way:

data ListWHNF (as :: [*]) where
    LZ :: ListWHNF '[]
    LS :: ListWHNF as -> ListWHNF (a ': as)

first' :: ListWHNF (a ': as) -> CatList (a ': as) -> CatList '[a]
first' _ (HCons a _) = HCons a HNil

main = print $ first' (LS $ LS LZ) (HCons (Cat 3) $ HCons (Cat True) HNil)

So first' now receives something, that looks like the length of a list. But can we do this statically? Not so fast:

data ListWHNF (as :: [*]) where
    LZ :: ListWHNF '[]
    LS :: ListWHNF as -> ListWHNF (a ': as)

data HList as ln where
    HNil  :: HList '[] LZ
    HCons :: a -> HList as ln -> HList (a ': as) (LS ln)

throws Data constructor LZ comes from an un-promotable type ListWHNF …. We cannot use indexed datatypes as indices in Haskell.

Having some sort of functional dependencies, that would allow to associate a term of one type and the weak head normal form of a term of another, we could probably do the trick, but I am not aware about anything like that in GHC (but I am not an expert). In Agda this is simply

_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0     = Lift ⊤
A ^ suc n = A × A ^ n

So if the only thing, we need to infer a list, is its length, then we can replace a list with n nested tuples. Abusing the notation, [?, ?] :: [*] becomes (? :: *, (? :: *, Lift ⊤)) and all these ? can now be inferred automatically among with the inhabitant of ⊤ (Agda's equivalent of ()). But in Agda there is no distinction between value-level and type-level programming, so there are no such problems at all.