[GHC] #15710: Should accept a type that needs coercion quantification
#15710: Should accept a type that needs coercion quantification -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider {{{ f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x f = error "uk" }}} Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being {{{ f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x }}} But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType 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 simonpj): In #14648 you argued that `(t1 ~# t2)` should not be a constraint, should not return True to `isPredTy`, and should not be an invisible parameter, implicitly instantiated at call sites. Here you seem to be arguing the exact opposite! I'm uncomfortable with forcing the the user to deal with both `(~)` and `(~#)`; I wanted the latter to be an implementation detail. Even putting it in a constraint tuple like `f :: (Num a, a ~ b) => blah` is problematic if `a~b` is unlifted/unboxed. Our "all constraints are boxed" story was working perfectly well right up to this, when we add coercion quantification. But I don't see a way to reconcile it with coercion quantification. Alas. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType 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): Yes, I'm arguing both sides -- but with good reason. `t1 ~# t2` is not a constraint ''today'', and thus it shouldn't respond to `isPredTy`. But this ticket is all about ''tomorrow'', when I do think it could become a constraint. Would we be more efficient if constraints could be strict and unboxed? I imagine "yes". If so, then the current story isn't working as well as it could be. As for tupling: we could make `( ... )` be an unboxed tuple if it's written to the left of `=>`. In the end, I just think of the parens and commas as concrete syntax for some unspecified abstract syntax that handles sets of constraints here. (This is not how I think of the argument to `Dict`, say, where order suddenly matters.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType 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 simonpj): Tupling: yes `f :: (Num a, Ord a) => blah` is ''already'' syntactic sugar for `f :: Num a => Ord a => blah`. But I'm more concerned about {{{ type C a b = (Num a, a ~ b) }}} and here it'd be much trickier (and unprincipled) to switch to unboxed tuples. Moreover, we do lots of constraint abstraction {{{ data Dict c where Dict :: c => Dict c }}} and we can't instantiate that polymorphic `c` with an unboxed tuple. So yes, I think we could have `Constraint` and `Constraint#` just as we have `Int` and `Int#`. But it's very uncomfortable to have to use `a ~# b` in a type if (but only if) the constraint is used in a dependent way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
Consider {{{ f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x f = error "uk" }}} Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being {{{ f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x }}} But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
New description: Consider {{{ f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x f = error "uk" }}} Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being {{{ f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x }}} But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here. These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see comment:5 in #15497 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType 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): When we get this, we can remove `Note [Emitting the residual implication in simplifyInfer]` in TcSimplify. See comment:5:ticket:15497. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12677 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #12677 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12677 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): #15870 is an example of someone actually trying this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC