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

Tom Ellis tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk
Thu Jan 12 16:24:12 UTC 2023

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.


More information about the Haskell-Cafe mailing list