Problem with type variable used boxed and unboxed. ("Impossible happened")

[gteege]

type A
f: all(a). #a -> a
ff: all(b,c). (b->c) -> ()

g: () -> ()
g () = ff[#A,A](f)

causes the error message:

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
cogent: bound: not comparable: (TCon "A" [] (Boxed False (Bits {allocSize = 0, allocOffset = 0})),TCon "A" [] Unboxed): 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-UjKKohV2oW3QCVdcuN0SY:Cogent.Compiler

Can be avoided by using two different type variables for f:

type A
f: all(a1,a2). #a1 -> a2
ff: all(b,c). (b->c) -> ()

g: () -> ()
g () = ff[#A,A](f)

[zilinc]

The fix b48becd is not quite right. We need to have TVar (Fin v) Banged Unboxed instead of separate TVarBang and TVarUnboxed in the core language, as a#! /= a! and a#! /= a# in general.

[zilinc]

#a is bad in general, as there's no way that we can determine the kind of it. E.g., if a : E, then #a can be either DSE (if a is a boxed record with no linear fields) or E (if a is a boxed record with linear fields).

[gteege]

The issue resulted when I tried to model an initialization function for a boxed record as an abstract generic function

  init: all(evt,vvt). (evt,#vvt) -> vvt

where evt is the type of an uninitialized ("empty") value (typically a record with all fields taken), and vvt is the type of the initialized ("valid") value (the normal record). The function takes as argument the pointer to the allocated but uninitialized heap area (of type evt) and the stack-allocated record content (of type #vvt), stores the content into the heap area and returns the pointer as a value of type vvt. Both evt and vvt are intended to be boxed types. One problem is that this cannot be expressed as a constraint in Cogent. So I interpreted # as an operator applicable to all types which will be the identity for non-boxed types.

Of course, as zilin commented, also for this application it is not known whether #vvt is linear or not, both is possible. But I would argue that for an abstract function that should not be a problem for Cogent, it must be dealt with by the person who implements the abstract function. The implementation described above would be correct for both cases, since it causes no sharing or discarding of linear values contained in #vvt values. But maybe I am wrong and Cogent is affected in some way when the abstract function is used in non-abstract Cogent functions?

[gteege]

More generally, there are type operators in Cogent which are only applicable to certain kinds of types, such as the take operator which is only applicable to records. However, there are no means to constrain type variables to such kinds of types. Note that the case described in my previous comment would even be better modeled using something like

  init: all(vvt :< record).(vvt take (..),#vvt) -> vvt

I tried to solve it using --flax-take-put, which lead to issue #307.

Perhaps extending the permissions by such constraints could be a better and more general solution.