cogent
cogent copied to clipboard
Impossible happened when combining # and !
The code
type T a = { x: #a }!
g: all(a). () -> T a
type S = { y : { z: U8 } }
f: () -> T S
f () = g[S] ()
causes the error message
Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
cogent: bound: not comparable: (TRecord [("z",(TPrim U8,False))] (Boxed False (Bits {allocSize = 0, allocOffset = 0})),TRecord [("z",(TPrim U8,False))] (Boxed True (Bits {allocSize = 0, allocOffset = 0}))): the 'impossible' happened!
If you see this, please report this bug to
<https://github.com/NICTA/cogent/issues>
CallStack (from HasCallStack):
error, called at src/Cogent/Compiler.hs:31:20 in cogent-2.9.0.0-MRVlC24fphLGNkexARYpV:Cogent.Compiler
It seems to me that the ! operator is not correctly propagated through the unbox operator.
Depends on the fix to #306 . Right now because we haven't quite decided yet how to deal with !
-ed and #
-ed type vars, we don't have a syntax in the core language for such a thing. As a result the compiler simply (wrongly) desugars that #a!
to a TVarUnboxed
, resulting the mismatch of types in the core tc (https://github.com/NICTA/cogent/blob/master/cogent/src/Cogent/Desugar.hs#L524).