#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