[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, Roles
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):

 In cleaning up `tcView`/`coreView` to handle the disparity between the
 type-checker and Core vis-a-vis `Constraint`/`Type`, I came across a
 problem: which function (`coreView` or `tcView`) to use in the pure
 unifier? I decided that `coreView` was necessary there, because the pure
 unifier is used for instance overlap detection, where a
 `Constraint`/`Type` confusion could cause type unsoundness.

 But then `polykinds/T11480b` failed. A simplification of the problem is
 this: We have a class `C :: forall k. (Type -> k) -> Constraint`. The
 solver goes looking for an instance `C Constraint Eq`. (This instance is
 well-kinded.) But it finds an instance `C Type Eq`. As far as Core is
 concerned, this found instance is also well-typed... but the solver then
 looks at `C Type Eq` and falls over because the instance looks ill-kinded
 to it.

 One solution to this is to have the caller of any entry point into the
 pure unifier choose which notion of equality (i.e. `tcView`'s version or
 `coreView`'s version) it wants. But it's unclear what the right choices
 are.

 Here are the competing concerns:

 1. We absolutely cannot have `type instance F Type = Int` and `type
 instance F Constraint = Bool`. That's begging for someone to write
 `unsafeCoerce`.

 2. We also don't want the solver to find the instance for `C Type` when it
 goes looking for `C Constraint`, as that's very confusing to a solver that
 thinks `Type` and `Constraint` are different.

 3. It would sure be nice to have both `Typeable Constraint` and `Typeable
 Type` be solvable.

 The only way I can think of resolving this is:
  - Forbid '''type''' instances that overlap w.r.t. `coreView`'s equality.
  - Allow '''class''' instances that overlap w.r.t. `coreView`'s equality.
 (After all, overlapping class instances can't cause unsoundness.
  - Use `tcView` when doing instance matching (for any instance flavor).

 This satisfies goals (1), (2), and (3). But it seems very squirrelly
 indeed to have different overlap checks for type instances and class
 instances. The only other alternative is to forbid `coreView` overlap for
 all instances and say that `Typeable Constraint` is insoluble, drastically
 reducing the set of `Typeable` things.

 I would love some thoughts from the crowd on this!

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