[Haskell-cafe] Unboxed, zero-width :~:/Refl?

[Tom Ellis]

On Thu, Jan 12, 2023 at 05:51:58PM +0200, Oleg Grenrus wrote:
> Because you have to actually compute `Refl` for it to be valid.

Sure, but an unboxed constraint would be unlifted, wouldn't it?

> Your a :~:# b doesn't work. you cannot define unboxedRefl:
> 
>     Top-level bindings for unlifted types aren't allowed:
>       unboxedRefl = Refl (##)

Ah, that's interesting.  Why is that?  I can't immediately see a
theoretical blocker.  There's a practical one, of course: strict
bindings are not allowed at the top level either, I guess to prevent
infinite loops.  Seems strange though.  Does OCaml not allow defining
constants at the top level?

> Also  a ~ b is *boxed* constraint, so you need to create it e.g.

That seems enough to make my scheme impossible.  By why is it boxed?
It doesn't seem like it actually needs any evidence to make it work.

Tom