Type inference with GADTs

Question

In the following code, I'm trying to match on the GADT constructor Cons to get the compiler to see that xs is non-empty:

{-# LANGUAGE DataKinds           #-} 
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-} 
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

import Data.Typeable

data Foo (ts :: [*]) where
  Nil :: Foo '[]
  Cons :: (Typeable t) => Foo ts -> Foo ( t ': ts)

foo :: Foo xs -> IO ()
foo Nil = print "done"
foo (Cons rest :: Foo (y ': ys)) = do
  print $ show $ typeRep (Proxy::Proxy y)
  foo rest

Unfortunately, this simple example fails to compile with GHC 8:

• Couldn't match type ‘xs’ with ‘y : ys’
  ‘xs’ is a rigid type variable bound by
    the type signature for:
      foo :: forall (xs :: [*]). Foo xs -> IO ()
  Expected type: Foo (y : ys)
    Actual type: Foo xs
• When checking that the pattern signature: Foo (y : ys)
    fits the type of its context: Foo xs
  In the pattern: Cons rest :: Foo (y : ys)
  In an equation for ‘foo’:
      foo (Cons rest :: Foo (y : ys))
        = print $ (show $ typeRep (Proxy :: Proxy y))

I know that type inference can be tricky with GADTs (e.g., #9695, #10195, #10338), but this is so simple...

What do I need to do to convince GHC that when I match on Cons, the GADT argument has at least one element?

Of course this example is simplified, but foo really has some recursive calls in it. I need to match on either the Cons case or the Nil case (elided), and naturally Nil :: Foo '[]. I really do need GHC to figure out xs ~ (y ': ys) based on the pattern match. — crockeea
@Alec I improved the example to demonstrate why I'm asking what I'm asking. I hate it when I oversimplify examples... — crockeea
Thanks! As a side note, this would be really useful here. :) — Alec

user2407038 user2407038 · Accepted Answer · 2017-03-16T09:33:09

All you need is a function to extract the Proxy t from a Foo (t ': ts):

fooFstType :: Foo (t ': ts) -> Proxy t 
fooFstType _ = Proxy

Note that since the type argument to Foo is t ': ts, not simply ts, you may refer to the type variable representing the first element in the type signature (as opposed to in the body, somehow, with ScopedTypeVariables).

Your function becomes

foo :: Foo xs -> IO ()
foo Nil = print "done"
foo f@(Cons rest) = do
  print $ show $ typeRep (fooFstType f)
  foo rest

Another possibility is to move the work to the type level:

type family First (xs :: [k]) :: k where 
  First (x ': xs) = x 

foo :: forall xs . Foo xs -> IO ()
foo Nil = print "done"
foo (Cons rest) = do
  print $ show $ typeRep (Proxy :: Proxy (First xs))
  foo rest

Type inference with GADTs

1 Answers