[GHC] #11715: Constraint vs *

[GHC]

#11715: Constraint vs *
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:  Typeable
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):

 Simon and I recently hit on a possible solution to this long-standing
 infelicity.

 1. Add a new constructor of `RuntimeRep` (of levity-polymorphism fame),
 `ConstraintRep`. We would then have `type Constraint = TYPE
 ConstraintRep`.

 Even though values of types of kind `Constraint` have the same runtime
 representation as values of types of kind `Type`, it is still OK to have
 ''more'' distinctions in the type system than are needed at runtime.

 With this change, we can have things like `Num a -> a` in Core (where
 there is no distinction between `=>` and `->`), and this would be well-
 kinded because `->` simply requires that both types have a kind of the
 form `TYPE blah` for some `blah`.

 GHC currently desugars one-method (and 0-superclass) classes to be
 newtypes, not proper datatypes. This is more efficient, of course, than
 making a new box to store the dictionary. But it means under this new
 scheme that we have a heterogeneous newtype coercion. For example:

 {{{#!hs
 class C a where
   meth :: a -> a
 }}}

 is desugared into

 {{{#!hs
 newtype C a = MkCDict { meth :: a -> a }
 }}}

 which produces a coercion

 {{{
 axC :: forall (a :: Type). C a ~R# (a -> a)
 }}}

 Under our new scheme, this coercion would be heterogeneous, because `C a
 :: TYPE ConstraintRep` and `(a -> a) :: TYPE LiftedRep`. Of course, GHC
 (now) handles heterogeneous equalities just fine, but there is a problem:
 GHC can extract a kind equality from a type equality via its `KindCo`
 coercion, captured in this typing rule:

 {{{
      co : (t1 :: k1) ~r# (t2 :: k2)
 -----------------------------------------
 KindCo co : (k1 :: Type) ~N# (k2 :: Type)
 }}}

 Note that the premise does not require any particular role on the
 coercion, while the conclusion is always nominal. With `KindCo` (and a few
 other coercion formers), we could derive a proof of `ConstraintRep ~N#
 LiftedRep` from `axC`. This is terrible.

 So:

 2. Require the coercion in `KindCo` to be nominal.

 This makes our equality relation a tiny bit weaker, but I don't think the
 lost expressiveness will ever bite. GHC does not currently export a
 heterogeneous version of representational equality (although such a thing
 exists internally), so users can't every really witness it. And the place
 where this is key is in decomposing `AppCo`s, but the roles around
 `AppCo`s mean that the coercion relating the arguments is always nominal.
 So I think it will work out; building GHC's libraries with this
 restriction should be an adequate test.

 One remaining problem is that GHC uses newtype axioms for substitutions
 in, e.g., newtype unwrapping/normalization. So a heterogeneous axiom is a
 bad idea. And I'm not yet sure how to fix this. The normal way to avoid
 heterogeneity is just to cast one side. But we can't do this here, because
 the coercion we would have to use proves that `Constraint ~N# Type`, which
 is precisely what we are trying to avoid! So I'm still a bit stuck on this
 point.

 Another possible way forward is to do (1), above, and stop encoding one-
 element classes as newtypes. This has negative performance implications,
 and so that makes me sad.

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