Type lits currently can't do anyyyy abstract reasoning. It can only decide if two concrete literals are equal or reduce an expression made from concrete literals to a new concrete literal.
For that reason I'm using peano style Nats in my own lib engineering. On Sunday, May 18, 2014, Herbert Valerio Riedel <[email protected]> wrote: > Hello again, > > ...while experimenting with TypeLits I stumbled over the following > simple case failing to type-check with GHC 7.8.2: > > {-# LANGUAGE DataKinds, GADTs #-} > > data List l t where > Nil :: List 0 t > Cons :: { lstHead :: t, lstTail :: List l t } -> List (l+1) t > > with the error message > > ,---- > | Could not deduce (l1 ~ l) from the context ((l + 1) ~ (l1 + 1)) > | bound by a pattern with constructor > | Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) > t, > | in an equation for ‘lstTail’ > | > | ‘l1’ is a rigid type variable bound by > | a pattern with constructor > | Cons :: forall t (l :: Nat). t -> List l t -> List (l + 1) t, > | in an equation for ‘lstTail’ > | > | ‘l’ is a rigid type variable bound by > | the type signature for lstTail :: List (l + 1) t -> List l t > | > | Expected type: List l t > | Actual type: List l1 t > | Relevant bindings include > | lstTail :: List l1 t > | lstTail :: List (l + 1) t -> List l t > | > | In the expression: lstTail > | In an equation for ‘lstTail’: > | lstTail (Cons {lstTail = lstTail}) = lstTail > `---- > > While the code below happily type-checks: > > {-# LANGUAGE DataKinds, GADTs #-} > > data Nat = Z | S Nat > > data List l t where > Nil :: List Z t > Cons :: { lstHead :: t, lstTail :: List n t } -> List (S n) t > > Is this a known issue with the TypeLit solver? > > Cheers, > hvr > _______________________________________________ > ghc-devs mailing list > [email protected] <javascript:;> > http://www.haskell.org/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
