type A = U32
three : A
three = 3
foo : A#[three] -> A
foo x = x@2
It doesn't normalise A to U32 before it converts things into the SMT language, which causes the compiler to crash. It may be due to the equations derived from the constant definitions (https://github.com/au-ts/cogent/blob/master/cogent/src/Cogent/TypeCheck/Solver/SMT.hs#L64), which are taken from the state, in which types are not normalised. Also observed on the wip-reftypes branch.
It doesn't normalise
AtoU32before it converts things into the SMT language, which causes the compiler to crash. It may be due to the equations derived from the constant definitions (https://github.com/au-ts/cogent/blob/master/cogent/src/Cogent/TypeCheck/Solver/SMT.hs#L64), which are taken from the state, in which types are not normalised. Also observed on thewip-reftypesbranch.