CODEWITHSUNDEEP
haskelltypesghc
Gowtham Kaki
Gowtham Kaki

Reputation: 377

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

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:

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

Upvotes: 3

Views: 159

Answers (2)

phadej
phadej

Reputation: 12123

Say we have following definition:

append VNil         v2 = v2
append (VCons x xs) v2 = VCons x (append xs v2)

It's obvious from the definition that:

append :: Vec a n -> Vec a m -> Vec a p

As if you don't mind the Nat index in Vec, it's HM-type and everything should go simply.

Then we could write out constraints for n, m and p:

appendIndex Zero m ~ m                          -- from VNil case
appendIndex (Succ n) m ~ Succ (appendIndex n m) -- from VCons case

I didn't read the JFP paper, but I think that OutsideIn can't solve this constraints. It has to be able to solve them without any context i.e. knowing that somewhere is Plus.

It could solve the constraint with something like (pseudosyntax, type lambda):

append :: Vec a n -> Vec a m -> Vec a (rec f (λ n → case n of { Zero -> m ; Succ n' -> Succ (f n') }))

And with even smarter compiler the anonymous definition of plus could be unified with Plus or Plus' when function is used.

It's worth taking advice from a simpler paper: FPH: First-class Polymorphism for Haskell,, especially for top-level definitions:

  • If type is HM it can be inferred
  • Other types (RankN) should be annotated, cannot be inferred.

As for non-trivial example, I guess there can't be one as GHC type language doesn't have (even non-recursive) anonymous type functions (AFAIK).

Even the quite simple (non-recursive in types) example fails

data NonEmpty :: * -> Bool -> * where
  VNil :: NonEmpty a False
  VCons :: a -> NonEmpty a b -> NonEmpty a True

append VNil         v2 = v2
append (VCons x xs) v2 = VCons x (append xs v2)

as it have to infer

appendIndex True b = True
appendIndex False b = b

which is essentially || on a type level. GHC doesn't support (yet?) function promotion. So you can't even write

append :: NonEmpty a x -> NonEmpty b y -> NonEmpty b (x '|| y)

But there are developments towards making it possible http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf

Upvotes: 4

dfeuer
dfeuer

Reputation: 48591

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)

Upvotes: 8

Related Questions