cogent icon indicating copy to clipboard operation
cogent copied to clipboard

Impossible happened when combining # and !

Open gteege opened this issue 5 years ago • 1 comments

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.

gteege avatar Dec 28 '19 18:12 gteege

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).

zilinc avatar Jan 02 '20 05:01 zilinc