[GHC] #11715: Constraint vs *

[GHC]

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

 As comment:63 says, this patch (available on the `wip/t11715` branch) is
 in limbo.

 What's the challenge? See
 [https://phabricator.haskell.org/D2038#inline-25457 this comment] on a
 related patch. The short version is that the design in comment:47 and in
 the [https://github.com/ghc-proposals/ghc-proposals/pull/32 ghc-proposal]
 require weakening `KindCo` to work only on nominal coercions. And
 Phab:D2038 requires it to work on representational ones. The decision was
 to punt on this patch in favor of that one.

 There is a somewhat-detailed plan of how to proceed, originally posted
 [https://mail.haskell.org/pipermail/ghc-devs/2017-February/013702.html
 here]:

  1. Hold off on Constraint v Type until after the branch is cut.
  2. Do what we can to mitigate Constraint v Type confusion vis-a-vis
 Typeable. (For example, make sure that there aren't Typeable instances for
 both, and have TcTypeable provide the Type instance whenever the
 Constraint instance is requested.)
  3. Advertise that GHC will be a little confused on this point, and that,
 as far as Typeable is concerned, Constraint and Type are synonymous.
  4. On the Constraint v Type patch, restore the full power of KindCo. This
 makes the type system broken, but I don't think the sky will come crashing
 down.
  5. Merge Constraint v Type after the branch is cut. This will make GHC
 HEAD unsound in a new way, but no one will notice unless they try.
  6. File a priority-highest bug to eliminate newtype-classes (which beget
 heterogeneous axioms in the Constraint/=Type world).
  7. Finish the first-class reification design and implement before 8.4.
  8. Remove newtype-classes, thus eliminating heterogeneous axioms and the
 unsoundness mentioned in (5).

 This plan was met with general applause.

 But a recent chat with Simon suggested a new direction, that would allow
 us to separate Constraint from Type while keeping the efficiency of
 newtype-classes. In brief:

   * Allow representational casts in kinds, resurrecting sections 5 and 6
 of an [http://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf
 unpublished paper of mine].

 Currently, all kind-casts (that is, all uses of `CastTy` to change the
 kind of a type) use nominal coercions. This means that if we separate
 Constraint from Type, any equating of `C a` with `a` (in `class C a where
 meth :: a`) will somehow lead to a nominal equality between Constraint and
 Type, precisely the situation we wish to avoid. But if we allow
 representational coercions in kinds, then we can arrange to have
 `Constraint ~R Type` but not `Constraint ~N Type`. Indeed this makes more
 intuitive sense, because `Constraint` and `Type` do have the same runtime
 representation, but we wish to keep them separate regardless.

 Sadly, representational coercions in kinds are troublesome, as described
 [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#RolesCoherenceandKinds
 here] and in that unpublished paper. The paper details a kind system that
 circumvents the problem, and thus presents a plausible way forward. But it
 requires yet more wrinkles in GHC's coercion language. Is this worth it?
 Perhaps. Previously, Simon vetoed that system as overly complicated. The
 nub of his argument was that there was no point in having roles in kind-
 coercions. But now, we have a reason to do this, so it might be well-
 advised to revisit that decision. It's also possible that any wisdom I
 have accumulated in the intervening years may come to bear and help us
 out.

 Another approach that we considered was to have three different, unrelated
 arrow types: `(->) :: TYPE r1 -> TYPE r2 -> Type`, `(=>) :: Constraint ->
 TYPE r -> Type`, `(=>) :: Constraint -> Constraint -> Type`, where the
 last one is used to build dictionaries. Having these arrows like this
 prevents the need for `KindCo` to work on representational coercions --
 thus removing the incompatibility between the original solution proposed
 in comment:47 and the work in Phab:D2038. This would work, and would allow
 us to keep `C a ~R a`, but then we couldn't have `(C a => a) ~R (a -> a)`,
 so the newtype-class efficiency would run out of gas fairly quickly.

 I do think, in the long run, that having representational coercions in
 kinds is the Right Answer, because it will be necessary to support
 promoting newtypes to kinds, necessary for full
 [http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf
 dependent types].

 I don't expect any action on this until the summer, at least, but I wanted
 to jot it all down.

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