[GHC] #14832: QuantifiedConstraints: Strengthening context causes failure
#14832: QuantifiedConstraints: Strengthening context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- With Simon's latest changes (ticket:14733#comment:9) this works: {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance Refl rel => Category (With rel) where id = With (.) = undefined }}} But strengthening the context with `Trans rel`: {{{#!hs instance (Refl rel, Trans rel) => Category (With rel) where }}} causes it to fail {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( J.hs, interpreted ) J.hs:15:10: error: • Could not deduce: rel xx zz from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 or from: (rel xx yy, rel yy zz) bound by a quantified context at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ J.hs:15:10: error: • Could not deduce: rel xx xx from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Strengthening context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): The same happens if we add {{{#!hs instance (Refl rel, forall xx. xx) => Category (With rel) where }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Strengthening context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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): GHC is very careful about picking instances. See http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html #overlapping-instances, esp the bit about "all instances that unify". The constraint `rel xx xx` matches both `(Refl rel)` and `(Trans rel)`; but the (head of) the former is an instance of the (head of) the latter so it should win. At least with overlapping instances on. (There's no way to add an OVERLAPPING pragama to an individual quantified constraint -- yet anyway.) The constraint `rel xx zz` could (if `zz` was further instantiated) match`(Refl rel)`, so GHC refains from picking it. `IncoherentInstnaces` might help. In short, right now I'm being very conservative about ambiguity. Once we pick the "wrong" path there is no way back -- GHC does no backtracking. I'm inclined to park this one until we have the basics nailed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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/14832#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Replying to [comment:2 simonpj]:
I'm inclined to park this one until we have the basics nailed.
That's fine, this isn't (doesn't seem to be) a show stopper. In this case I can encode these properties as a type class (`(:-)`-enriched categories) {{{#!hs type ConstraintCat ob = ob -> ob -> Constraint class ConstraintCategory (cat::ConstraintCat ob) where cid :: () :- cat a a comp :: (cat a b, cat b c) :- cat a c instance CCategory cat => Category (With cat) where id :: forall a. With cat a a id = case cid :: () :- cat a a of Dict -> With (.) :: forall b c a. With cat b c -> With cat a b -> With cat a c With . With = case ccomp :: (cat a b, cat b c) :- cat a c of Dict -> With }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 RyanGlScott): Using the latest commit on the `wip/T2893` branch, this program now gives you a stack overflow! {{{ $ inplace/bin/ghc-stage2 --interactive ../Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( ../Bug.hs, interpreted ) ../Bug.hs:15:10: error: • Reduction stack overflow; size = 201 When simplifying the following type: rel xx yy0 Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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): What is "this program"? The one in comment:4 uses `CCategory` but does not define it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 RyanGlScott): I'm referring to the original program itself: {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance (Refl rel, Trans rel) => Category (With rel) where id = With (.) = undefined }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Replying to [comment:6 simonpj]:
What is "this program"? The one in comment:4 uses `CCategory` but does not define it.
`ConstraintCategory` was meant to be `CCategory`, I changed it to reflect that -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Replying to [comment:7 RyanGlScott]:
I'm referring to the original program itself:
The original program still gives a stack overflow with [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest changes]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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):
The original program still gives a stack overflow with latest changes.
And so it should. You have a "given" `(Trans rel)`, where {{ type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) }}} So if you want to solve `[W] rel t1 t2` (for some type `t1` or `t2`, this local instance (quantified constraint) matches. We can solve it by solving {{{ [W] rel t1 alpha [W] rel alpha t2 }}} where `alpha` is a fresh unification variable (corresponding to `yy` in the definition of `Trans rel`. But then each of those two constraints can be solved once more with this over-general local instance -- and now we hare four constraints. And so on. You used `UndecidableInstances` and sure enough you wrote an infinite loop. I say there is no bug here. The same thing wold happen if you wrote {{{ instance (C a x, C x b) => C a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Is there hope for the user to guide this process and leaving the definition of `Trans` intact (not having to create `CCategory`)? If this were a rank-2 function we can explicitly instantiate `xx` `yy` `zz` {{{#!hs foo :: R X Y -> R Y Z -> (forall xx yy zz. (R xx yy, R yy zz) => R xx zz) -> R X Y foo xy yz f = f @X @Y @Z (xy, yz) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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):
Is there hope for the user to guide this process
You want to write a ''term-level'' function that can be used a theorem in solving ''type-level'' constraints. This also came up, I think, in #14822. Of course, this is much what happens in many proof assistants. Perhaps we can learn from them. Personally, I don't see a direct way to do this; but perhaps others with a broader perspective, and a bit more time, might do so. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Replying to [comment:12 simonpj]:
You want to write a ''term-level'' function that can be used a theorem in solving ''type-level'' constraints.
That's right. Here are some thoughts I have on a [https://gist.github.com/ekmett/b26363fc0f38777a637d#file-categories- hs-L84 meatier example] I just ran into. Each category in `hask` has an associated constraint for objects (`Ob cat a`). If `a` is an object of `Dom f` and `f` is a functor then `f a` must be an object of `Cod f` {{{#!hs ob :: Functor f => Ob (Dom f) a :- Ob (Cod f) (f a) ob = Sub (source (fmap id)) }}} Constructing this relies crucially on `fmap` and friends at the term level. The user has to pry `ob` open (at the right type) (here they just wanted to write `id = Nat id`) {{{#!hs id = Nat id1 where id1 :: forall f x. (Functor f, Ob (Dom f) x) => Cod f (f x) (f x) id1 = id \\ (ob :: Ob (Dom f) x :- Ob (Cod f) (f x)) }}} It actually works today to add this implication to the superclass context of `Functor f` but GHC will not use it and refuses to take our (term- level) `ob` into account {{{#!hs type MapOb f = (forall x. Ob (Dom f) x => Ob (Cod f) (f x) :: Constraint) class (MapOb f, ..) => Functor f .. }}} I see several issues for what I just presented 1. `Dom` / `Cod` are type families (#14860) 2. We can't convert from `a :- b` to `Dict (a => b)` (#14822) 3. Ignoring **1.** / **2.** for now, how can we even use `ob` to witness `MapOb f`? One idea is to allow pattern matching outside of `case` expressions or indeed outside any definition, so we could write {{{#!hs reifyC :: (a :- b) -> Dict (a => b) reifyC = error "let's assume this for a second" class MapOb f => Functor f where -- This brings `MapOb f' into scope for the whole instance Dict <- reifyC (ob @_ @_ @f) }}} Am I off base here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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): See also #14937. I'm too snowed under to think about this -- but open to worked-out suggestions if you want to progress it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): Solve this: [https://gist.github.com/Icelandjack/93cf64878e286ed6378adf8fc0e7c200 gist] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14832: QuantifiedConstraints: Adding to the context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints 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 RyanGlScott): * keywords: QuantifiedConstraints wipT2893 => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14832#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC