[darcs-devel] [patch1880] decouple RepoPatchV3 impl from NamedPrim

Benjamin Franksen ben.franksen at online.de
Thu Aug 29 12:51:08 UTC 2019


>> Sure. It still bugs me that we have to go through (unsafely) unpacking
>> and then repacking the Sealed here. I have tried lots of alternatives
>> but nothing works that isn't essentially the same as what we have now.
>> IMO the strictness restriction for pattern matching existentials (and
>> GADTs in general) is really annoying and I wish they would lift that. I
>> opened an issue here: https://gitlab.haskell.org/ghc/ghc/issues/17130
> 
> If the GADT embeds a proof then matching on it has to be strict, or you
> can get an unsound program, e.g. you could write
> 
>  case undefined :: Int :~: Bool of
>   ~Refl -> 5 :: Bool
> 
> But that's not true of a pure existential, so some kind of restricted
> lazy match would be possible in theory.

I see. Thanks for the good explanation.

Cheers
Ben



More information about the darcs-devel mailing list