GHC could not infer types in presence of GADTs and Type Families

Question

I have a simple length-indexed vector type and an append function over length-indexed vectors:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

module LengthIndexedList where

  data Zero
  data Succ a

  type family Plus (a :: *) (b :: *) :: *
  type instance Plus Zero b = b
  type instance Plus (Succ a) b = Succ (Plus a b)

  data Vec :: * -> * -> * where
    VNil :: Vec a Zero
    VCons :: a -> Vec a n -> Vec a (Succ n)

  -- If you remove the following type annotation, type inference
  -- fails.
  -- append :: Vec a n1 -> Vec a n2 -> Vec a (Plus n1 n2)
  append v1 v2 = case v1 of
    VNil -> v2
    (VCons x xs) -> VCons x (append xs v2)

Compilation fails as GHC cannot infer a type for the append function. I understand that type inference is tricky in presence of GADTs and Type Families partly due to polymorphic recursion. Nevertheless, as per Vytiniotis et al's JFP paper GHC7's type inference should work in presence of "type classes + GADTs + type families". In this context, I have two questions:

Why isn't type inference working for the above example (I am using GHC7)?
What is a non-trivial example involving GADTs and Type Functions (like the append above) for which GHC can infer types?

dfeuer dfeuer · Accepted Answer · 2015-01-14T01:56:51

I haven't read more than a drop of the paper, which is well over my head, but I believe the problem is almost certainly caused by the type family. You have a function of type

Vec a n1 -> Vec a n2 -> Vec a (Plus n1 n2)

but type inference, in principle, has no way to recognize that. I could add to your code a second type family,

type family Plus' (a :: *) (b :: *) :: *
type instance Plus' Zero b = b
type instance Plus' (Succ a) b = Succ (Plus' a b)

that looks just like Plus but with a different name. Inference has no way to figure out whether you want Plus or Plus'. Inference never chooses, and never lets itself get into a position where it might have to choose (without some really unpleasant things like IncoherentInstances). So inference could only be valid here if it were valid without Plus existing. I don't know nearly enough about the theory behind type checking, but I don't think type families can be inferred out of nowhere.

I believe what the paper means is that inference remains useful in the presence of all these things, and remains just as good as it is without them. You can, for example, write code that uses your append function and that does not have a type signature:

append3 a b c = a `append` b `append` c

Extra bonus note: DataKinds and closed type families make some of the code rather easier to understand. I would write your code like this:

data Nat = Zero | Succ Nat

type family Plus (a :: Nat) (b :: Nat) :: Nat where
  Plus Zero b = b
  Plus (Succ a) b = Succ (Plus a b)

data Vec :: * -> Nat -> * where
  VNil :: Vec a Zero
  VCons :: a -> Vec a n -> Vec a (Succ n)

GHC could not infer types in presence of GADTs and Type Families

2 Answers