[GHC] #15710: Should GHC accept a type signature that needs coercion quantification?

[GHC]

#15710: Should GHC accept a type signature that needs coercion quantification?
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Back when I was implementing `-XTypeInType`, your "problem" at the end was
 indeed a problem. There are some notes (meant mainly for myself)
 [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality
 here].

 Briefly, the problem was: how should we interpret a user-written `~`?
 Should it be a lifted/boxed thing or an unlifted/unboxed thing? If it's
 lifted, then we can abstract over it (e.g., write `Dict (a ~ b)`, where
 `Dict :: Constraint -> Type`). If it's unlifted, we can write the program
 in the original ticket.

 However, we now have a robust levity polymorphism mechanism, meaning that
 we can now abstract over unlifted things quite handily. There has also
 been recent musing about strict constraints, which fits in nicely. So,
 here's a sketch for how to do this.

 1. Introduce `CONSTRAINT :: RuntimeRep -> Type`. `Constraint` becomes a
 synonym for `CONSTRAINT LiftedRep`.

 2. Existing constraints would continue to have kind `Constraint`.

 3. Give `~` this new kind: `(~) :: forall k. k -> k -> CONSTRAINT
 (TupleRep '[])` -- essentially saying that `~` is strict and erases to 0
 bits.

 Really, what I've done here is made the user-facing equality `~` the same
 as the internal equality `~#`. (This will make even more sense when `~#`
 is homogeneous, like `~` is.)

 One might wonder about deferred type errors. I claim that this is a red
 herring. Since GHC 8.0, GHC has been strict in equality errors anyway.
 This is described in #11197. The solution is conceptually simple (but no
 one has implemented it yet): aggressively float-in case-matches on
 deferred type errors.

 One might also wonder about `Dict (a ~ b)` in this brave new world. It's
 true that the traditional `Dict` won't work here, but any user could
 define a `Dict#` that would, by abstracting over erased, strict
 constraints. Perhaps this change would be breaking enough that we'd need
 to keep `~` lifted and introduce a new name for the unlifted equality that
 could be used in coercion quantification, but I think we can debate that
 problem separately from the general design. (Note that it's very easy for
 a user to introduce a lifted equality type that wraps the unlifted one.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15710#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler