Can't match type `1+0` with `1`. (TypeNats addition doesn't reduce)
Here are two examples illustrating my problem:
(test2 and test3 produce the errors when the line that don't work are uncommented) This is a file:
--file: Scratch.hs {-# Language DataKinds, KindSignatures, TypeOperators #-}
import GHC.TypeLits
test1 = sing :: Sing (1) --works
--test2 = sing :: Sing (1+0) --doesn't
data F (n::Nat) = F ()
f :: F n -> F n -> () f _ _ = ()
x = F () :: F (1) --works
--x = F () :: F (1+0) --doesn't
y = F () :: F (1)
test3 = f x y
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | libraries/base |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |