Impredicativity bug: Church2 test gives a rather confusing error with the HEAD
The Church2 test gives a rather confusing error with the HEAD:
Church2.hs:27:14: Couldn't match expected type `CNat' against inferred type `(a -> a) -> a -> a' Expected type: CNat -> CNat Inferred type: CNat -> CNat In the first argument of `n', namely `(mul m)' In the expression: n (mul m) n1
In particular the lines
Expected type: CNat -> CNat Inferred type: CNat -> CNat
are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.
|Component||Compiler (Type checker)|
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information