CODEWITHSUNDEEP
haskellghc
crockeea
crockeea

Reputation: 21811

Type inference with GADTs

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?

Upvotes: 2

Views: 143

Answers (1)

user2407038
user2407038

Reputation: 14578

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

Upvotes: 3

Related Questions