#15710: Should GHC accept a type signature that needs coercion quantification? -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: 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): Back when I was implementing `-XTypeInType`, your "problem" at the end was indeed a problem. There are some notes (meant mainly for myself) [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unl... here]. Briefly, the problem was: how should we interpret a user-written `~`? Should it be a lifted/boxed thing or an unlifted/unboxed thing? If it's lifted, then we can abstract over it (e.g., write `Dict (a ~ b)`, where `Dict :: Constraint -> Type`). If it's unlifted, we can write the program in the original ticket. However, we now have a robust levity polymorphism mechanism, meaning that we can now abstract over unlifted things quite handily. There has also been recent musing about strict constraints, which fits in nicely. So, here's a sketch for how to do this. 1. Introduce `CONSTRAINT :: RuntimeRep -> Type`. `Constraint` becomes a synonym for `CONSTRAINT LiftedRep`. 2. Existing constraints would continue to have kind `Constraint`. 3. Give `~` this new kind: `(~) :: forall k. k -> k -> CONSTRAINT (TupleRep '[])` -- essentially saying that `~` is strict and erases to 0 bits. Really, what I've done here is made the user-facing equality `~` the same as the internal equality `~#`. (This will make even more sense when `~#` is homogeneous, like `~` is.) One might wonder about deferred type errors. I claim that this is a red herring. Since GHC 8.0, GHC has been strict in equality errors anyway. This is described in #11197. The solution is conceptually simple (but no one has implemented it yet): aggressively float-in case-matches on deferred type errors. One might also wonder about `Dict (a ~ b)` in this brave new world. It's true that the traditional `Dict` won't work here, but any user could define a `Dict#` that would, by abstracting over erased, strict constraints. Perhaps this change would be breaking enough that we'd need to keep `~` lifted and introduce a new name for the unlifted equality that could be used in coercion quantification, but I think we can debate that problem separately from the general design. (Note that it's very easy for a user to introduce a lifted equality type that wraps the unlifted one.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler