search

yav / type-nat-solver

A plugin for solving numeric constraints in GHC's type-checker
Other
50 stars 5 forks source link

Panic instead of type error #1

Closed yav closed 9 years ago

yav commented 9 years ago

The plugin has gotten out of wack with GHC, so with 7.10 this panics instead of just giving an error.

data Nat1 :: Nat -> * where
  Zero :: Nat1 0
  Succ :: Nat1 n -> Nat1 (n + 1)

add :: Nat1 m -> Nat1 n -> Nat1 (m + n + 1)
add Zero x      = x
add (Succ x) y  = Succ (add x y)