#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#RolesCoheren... 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