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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information