#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