[GHC] #7967: With dependent types, error reported in seemingly unrelated function

6 Jun 2013

      #7967: With dependent types, error reported in seemingly unrelated function
-----------------------------+----------------------------------------------
Reporter:  goldfire          |          Owner:                  
    Type:  bug               |         Status:  new             
Priority:  normal            |      Component:  Compiler        
 Version:  7.7               |       Keywords:  DataKinds, GADTs
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
 Failure:  None/Unknown      |      Blockedby:                  
Blocking:                    |        Related:                  
-----------------------------+----------------------------------------------
 In doing some routine dependently typed hackery, I wrote the following:

 {{{
 {-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}

 data Nat = Zero | Succ Nat

 data SNat :: Nat -> * where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)

 data HList :: [*] -> * where
   HNil :: HList '[]
   HCons :: h -> HList t -> HList (h ': t)

 data Index :: Nat -> [*] -> * where
   IZero :: Index Zero (h ': t)
   ISucc :: Index n l -> Index (Succ n) (h ': l)

 type family Lookup (n :: Nat) (l :: [*]) :: *
 type instance Lookup Zero (h ': t) = h
 type instance Lookup (Succ n) (h ': t) = Lookup n t

 hLookup :: Index n l -> HList l -> Lookup n l
 hLookup IZero (HCons h _) = h
 hLookup (ISucc n) (HCons _ t) = hLookup n t
 hLookup _ _ = undefined
 }}}

 So far, so good. But, I wanted a way to convert `SNat`s to `Index`es. When
 I add the (wrong) code below

 {{{
 sNatToIndex :: SNat n -> HList l -> Index n l
 sNatToIndex SZero HNil = IZero
 }}}

 I get an error in the second clause of `hLookup`, '''even though I haven't
 touched `hLookup`'''. (I also get an error in `sNatToIndex`, but that
 one's OK.)

 The error is this:

 {{{
 /Users/rae/temp/Bug.hs:23:33:
     Couldn't match type ‛t1’ with ‛Lookup n l’
       ‛t1’ is untouchable
         inside the constraints (l ~ (':) * h1 t)
         bound by a pattern with constructor
                    HCons :: forall h (t :: [*]). h -> HList t -> HList
 ((':) * h t),
                  in an equation for ‛hLookup’
         at /Users/rae/temp/Bug.hs:23:20-28
     Expected type: Lookup n l
       Actual type: Lookup n1 l1
     Relevant bindings include
       hLookup :: Index n l -> HList l -> Lookup n l
         (bound at /Users/rae/temp/Bug.hs:22:1)
     In the expression: hLookup n t
     In an equation for ‛hLookup’:
         hLookup (ISucc n) (HCons _ t) = hLookup n t
 }}}

 This was tested with 7.7.20130528.

-- 
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7967
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler