[GHC] #16252: QuantifiedConstraints: lack of inference really is a problem
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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: -------------------------------------+------------------------------------- I've been debugging an issue that boils down to: quantified constraints are completely ignored during type inference. For example, in this program: {{{#!hs {-# language QuantifiedConstraints #-} module QC where data A f = A (f Int) eqA :: forall f. (forall x. Eq x => Eq (f x)) => A f -> A f -> Bool eqA (A a) (A b) = a == b eqA' :: (forall x. Eq x => Eq (f x)) => A f -> A f -> Bool eqA' = let g = eqA in g }}} `eqA'` won't compile because `g` gets generalised to `forall f. A f -> A f -> Bool`. I know this has been discussed (and dismissed) in tickets such as #2256 and #14942, but I really think it's a problem. In my example, I can get the code compiling by turning on ScopedTypeVariables and giving `g` an annotation. But I don't always have this liberty. For example, in the `deriving-compat` library there's Template Haskell that generates definitions containing `let`s, and when a quantified constraint is present these splices don't type check for the same reason `eqA'` doesn't. The solution here involves a pull request to `deriving-compat` that uses ScopedTypeVariables to annotate the problematic `let`s. But I really think that none of this should be necessary. The reference implementation of QCs (https://github.com/gkaracha/quantcs-impl) doesn't seem to have this problem. Is there anything I'm missing? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 simonpj): Interesting! I can see what is happening. Given a binding `g = rhs`, GHC infers all the constraints C from `rhs` and tries to generalise. Currently that works as follows (`simplifyInfer`) 1. `approximateWC`: find `quant_pred_candidates`, the subset of constraints in C over which we could conceivably quantify. 2. Pick a set of `quant_pred_candidates` to quantify over 3. Crucially, do not generalise over any type variable free in a constraint we decide not to generalise in Step 2. (If we generalise over that type variable, the constraint will probably become insoluble.) The problem is that we don't account for constraints (such as implication constraints) that Step 1 discards! We do generalise over their type variables, and they duly become insoluble. That's why your definition of `g` is being generalised. Solution: don't generalise over any type variable free in a constraint that we can't quantify. I'm quite surprised this has not come up before. The fix will be a big fiddly but not really hard. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 lightandlight): What does it mean to 'quantify over a constraint' here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 lightandlight): Okay, I've thought about this for a little bit: Why shouldn't the implication constraint be considered part of `quant_pred_candidates`? It seems to me that the error is in discarding it as a candidate in the first place. In other words, I would expect `g`'s inferred type to be `(forall x. Eq x => Eq (f x)) => A f -> A f -> Bool`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 lightandlight): I've tried to implement the advice as described: excluding variables from generalisation when they appear in un-quantifiable constraints (collecting said variables in `approximateWC`, and removing them from `qtvs` in `simplifyInfer`). I now have an escaped skolem error. I think this is the relevant portion of the trace: {{{ {f1_a26[sk:1], f_a2c[sk:2]} g_ah :: forall (a :: (* -> *) -> *). a f_a2c[sk:2] -> a f_a2c[sk:2] -> Bool, eqA'_a28 :: a_a27[sk:1] f_a26[sk:1] -> a_a27[sk:1] f_a26[sk:1] -> Bool, eqA :: forall (f :: * -> *) (a :: (* -> *) -> *). (forall x. Eq x => Eq (f x)) => a f -> a f -> Bool, }}} Is it likely that I've forgotten some important call? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 simonpj):
Why shouldn't the implication constraint be considered part of quant_pred_candidates?
It's always sound to quantify over any constraints you can't solve. But in many cases that'll simply push type errors from the definition site to the call site of the function. There are many constraints we don't quantify over as you'll see in `pickQuantifiableConstraints`. I think it's better (more explicit, more comprehensible) just to provide a type signature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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 lightandlight): Okay. Do you have any advice regarding my current issue? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC