[GHC] #10195: GHC forgets constraints when matching on GADTs
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Here's a relatively short piece of code that doesn't compile: {{{#!hs {-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs, ConstraintKinds, KindSignatures, FlexibleInstances #-} module Foo where import GHC.Exts data Foo m zp r'q = Foo zp data Dict :: Constraint -> * where Dict :: a => Dict a type family BarFamily a b :: Bool class Bar m m' instance (BarFamily m m' ~ 'True) => Bar m m' magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq) magic = error "" getDict :: a -> Dict (Num a) getDict _ = error "" fromScalar :: r -> c m r fromScalar = error "" foo :: (Bar m m') => c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq) foo b (Foo sc) = let scinv = fromScalar sc in case getDict scinv of Dict -> magic $ scinv * b }}} GHC complains that it {{{ cannot deduce (BarFamily m m' ~ 'True) arising from a use of `magic` }}} in the definition of `foo`. Of course this is silly: `magic` requires `Bar m m'`, which is supplied as a constraint to `foo`. So GHC is forgetting about the constraint on `foo` and instead trying to satisfy the generic instance of `Bar` which has the constraint `(BarFamily m m' ~ 'True)`. I've found no less than six different ways to poke this code to make it compile, and some of them seem to reveal dangerous/unexpected behavior. The following are all deltas from the original code above and result in compiling code. 1. Add `ScopedTypeVariables` and give `scinv` an explicit signature: {{{ let scinv = fromScalar sc :: c m z in ... }}} I'm not sure why this would make GHC suddenly realize that it already has the constraint `Bar m m'`, but it seems to. (What it definitely does *not* do is result in a `BarFamily m m' ~ 'True` constraint.) 2. Remove the instance for `Bar`. This seems highly suspicious: the presence (or lack thereof) of an instance changes how GHC resolves the constraint in `foo`. 3. Change the constraint on `foo` to `BarFamily m m' ~ 'True`. In this case, GHC does *not* forget the constraint on `foo` and successfully uses it to satisfy the instance of `Bar`. Why does GHC forget about `Bar m m'` but not `BarFamily m m' ~ 'True`? 4. Add the superclass constraint `BarFamily m m' ~ 'True` to class `Bar`. Adding this constraint either makes GHC find the `Bar m m'` constraint on `foo` or, even more bizarrely, GHC still forgets about `Bar m m'` but manages to get the superclass constraint from `Bar m m'` and uses it to satisfy the instance. 5. Add `PolyKinds`. Not sure why this would affect anything. 6. Change the signature of `fromScalar` to `r -> s`. Not sure why this would affect anything. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rwbarton): I'm no expert on this part of the compiler, but it looks like GHC reduces the wanted constraint `Bar m m'` (from the use of `magic`) to `BarFamily m m' ~ 'True` (because of the `Bar` instance), and then it can no longer deduce that from `Bar m m'`. A peculiar scenario. It certainly looks wrong though, and FWIW GHC 7.6.3 accepts the program. The robust workaround is to add the superclass constraint `BarFamily m m' ~ 'True` to `Bar m m'`, since then (as you describe as "even more bizarrely") GHC can deduce either of `BarFamily m m' ~ 'True` and `Bar m m'` from the other, and then can't get stuck in this kind of situation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by crockeea): Can you confirm in 7.10? Since we have no idea what's causing the issue, nor exactly what "this situation" is, it's possible this behavior could occur for a less generic instance in a situation where the instance constraint can't just be trivially promoted to a superclass constraint. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rwbarton): Yes, the original program fails to compile in 7.8.1, 7.10-rc-something, and HEAD, though I didn't try your variations to see if they have the same behavior also. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Interesting. One problem with this code is that it sports some overlapping instances. Your local `Bar m m'` constraint overlaps with the global `Bar m m'` instance. It's not terribly surprising to me that GHC gets confused here. This is a dark corner of `FlexibleInstances`. Part of the problem is that it's hard for GHC to know what the type of `magic $ scinv * b` should be. Due to the GADT pattern-match, it doesn't want to guess that the type should be `Foo m zp (c m' zq)`, as that choice might be ignoring some information gained in the pattern-match. My guess is that some of your deltas cause GHC to deduce that no equalities are learned in the pattern-match, and thus that result type inference is safe. In any case, I don't think GHC is "forgetting" anything here. It's just choosing one seemingly-viable route toward a solution (the global instance) instead of another, the local constraint. I do agree that this behavior is somewhat disconcerting, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by crockeea): goldfire: In what sense does the `Bar m m'` constraint overlap with the instance? As far as I was aware, it would be impossible to have "overlapping" instances with just a single instance. This is likely just a misunderstanding of the term on my part. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): I'm perhaps abusing the term "overlap". What I mean here is that GHC has two routes with which to satisfy a `Bar m m'` constraint. Let's rename variables in the global instance for clarity: `instance (BarFamily b b' ~ 'True) => Bar b b'`. During type inference, GHC has to solve a `Bar p q` constraint, for some `p` and some `q`. If, at this point during inference, it knows `p ~ m` and `q ~ m'`, GHC will prefer the local constraint `Bar m m'`. Otherwise, if we don't yet know enough about `p` and `q`, it will use the global instance and then require `BarFamily p q ~ 'True`. Even if we later learn that `p ~ m` and `q ~ m'`, it's too late to use the `Bar m m'` constraint. I do know that GHC "tries hard" to resolve equality constraints before class constraints, but ''guaranteeing'' that this happens may be impossible. So, you'll end up with situations like these. I'd be quite curious for Simon's input here. He's on holiday at the moment, but I'm sure he'll chime in ere too long. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by crockeea: Old description:
Here's a relatively short piece of code that doesn't compile:
{{{#!hs {-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs, ConstraintKinds, KindSignatures, FlexibleInstances #-}
module Foo where
import GHC.Exts
data Foo m zp r'q = Foo zp data Dict :: Constraint -> * where Dict :: a => Dict a
type family BarFamily a b :: Bool class Bar m m' instance (BarFamily m m' ~ 'True) => Bar m m'
magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq) magic = error "" getDict :: a -> Dict (Num a) getDict _ = error "" fromScalar :: r -> c m r fromScalar = error ""
foo :: (Bar m m') => c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq) foo b (Foo sc) = let scinv = fromScalar sc in case getDict scinv of Dict -> magic $ scinv * b }}}
GHC complains that it {{{ cannot deduce (BarFamily m m' ~ 'True) arising from a use of `magic` }}} in the definition of `foo`. Of course this is silly: `magic` requires `Bar m m'`, which is supplied as a constraint to `foo`. So GHC is forgetting about the constraint on `foo` and instead trying to satisfy the generic instance of `Bar` which has the constraint `(BarFamily m m' ~ 'True)`.
I've found no less than six different ways to poke this code to make it compile, and some of them seem to reveal dangerous/unexpected behavior. The following are all deltas from the original code above and result in compiling code.
1. Add `ScopedTypeVariables` and give `scinv` an explicit signature: {{{ let scinv = fromScalar sc :: c m z in ... }}} I'm not sure why this would make GHC suddenly realize that it already has the constraint `Bar m m'`, but it seems to. (What it definitely does *not* do is result in a `BarFamily m m' ~ 'True` constraint.)
2. Remove the instance for `Bar`. This seems highly suspicious: the presence (or lack thereof) of an instance changes how GHC resolves the constraint in `foo`.
3. Change the constraint on `foo` to `BarFamily m m' ~ 'True`. In this case, GHC does *not* forget the constraint on `foo` and successfully uses it to satisfy the instance of `Bar`. Why does GHC forget about `Bar m m'` but not `BarFamily m m' ~ 'True`?
4. Add the superclass constraint `BarFamily m m' ~ 'True` to class `Bar`. Adding this constraint either makes GHC find the `Bar m m'` constraint on `foo` or, even more bizarrely, GHC still forgets about `Bar m m'` but manages to get the superclass constraint from `Bar m m'` and uses it to satisfy the instance.
5. Add `PolyKinds`. Not sure why this would affect anything.
6. Change the signature of `fromScalar` to `r -> s`. Not sure why this would affect anything.
New description: Here's a relatively short piece of code that doesn't compile: {{{#!hs {-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs, ConstraintKinds, KindSignatures, FlexibleInstances #-} module Foo where import GHC.Exts data Foo m zp r'q = Foo zp data Dict :: Constraint -> * where Dict :: a => Dict a type family BarFamily a b :: Bool class Bar m m' instance (BarFamily m m' ~ 'True) => Bar m m' magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq) magic = undefined getDict :: a -> Dict (Num a) getDict _ = undefined fromScalar :: r -> c m r fromScalar = undefined foo :: (Bar m m') => c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq) foo b (Foo sc) = let scinv = fromScalar sc in case getDict scinv of Dict -> magic $ scinv * b }}} GHC complains that it {{{ cannot deduce (BarFamily m m' ~ 'True) arising from a use of `magic` }}} in the definition of `foo`. Of course this is silly: `magic` requires `Bar m m'`, which is supplied as a constraint to `foo`. So GHC is forgetting about the constraint on `foo` and instead trying to satisfy the generic instance of `Bar` which has the constraint `(BarFamily m m' ~ 'True)`. I've found no less than six different ways to poke this code to make it compile, and some of them seem to reveal dangerous/unexpected behavior. The following are all deltas from the original code above and result in compiling code. 1. Add `ScopedTypeVariables` and give `scinv` an explicit signature: {{{ let scinv = fromScalar sc :: c m z in ... }}} I'm not sure why this would make GHC suddenly realize that it already has the constraint `Bar m m'`, but it seems to. (What it definitely does *not* do is result in a `BarFamily m m' ~ 'True` constraint.) 2. Remove the instance for `Bar`. This seems highly suspicious: the presence (or lack thereof) of an instance changes how GHC resolves the constraint in `foo`. 3. Change the constraint on `foo` to `BarFamily m m' ~ 'True`. In this case, GHC does *not* forget the constraint on `foo` and successfully uses it to satisfy the instance of `Bar`. Why does GHC forget about `Bar m m'` but not `BarFamily m m' ~ 'True`? 4. Add the superclass constraint `BarFamily m m' ~ 'True` to class `Bar`. Adding this constraint either makes GHC find the `Bar m m'` constraint on `foo` or, even more bizarrely, GHC still forgets about `Bar m m'` but manages to get the superclass constraint from `Bar m m'` and uses it to satisfy the instance. 5. Add `PolyKinds`. Not sure why this would affect anything. 6. Change the signature of `fromScalar` to `r -> s`. Not sure why this would affect anything. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): I understand what is going on here. We get this constraint from the call to `magic`: {{{ forall[2] c m m' zp. Bar m m' => forall[3]. Num (c m zp) => Bar meta[2] m', meta[2]~m }}} The [2] and [3] are the "untouchable" levels, and `meta[2]` is a level-2 unification variable. When checking whether we can safely fire the top- level instance `(Bar b b')`, we try to ''unify'' the given `Bar m m'` with `Bar meta[2] m'`. The unification variable `meta[2]` is untouchable, so we wrongly made it behave like a skolem in this unification, so the unification failed, and so we fired the top-level instance. But the `(meta[2] ~ m)` constraint, if allowed to float out and then fire, will make the `Bar meta[2] m'` turn into `Bar m m'`, which can then be discharged by the given `Bar m m'`. So the mistake here is being a bit too eager when asking "is the top-level instance the only one that could apply?". The fix is easy. But of course it means that fewer top-level instances will fire, so it's possible that it will break other examples that currently "work". But rightly so, I think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.4
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: merge Priority: normal | Milestone: 7.10.2 Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | typecheck/should_compile/T10195 Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => typecheck/should_compile/T10195 * milestone: => 7.10.2 Comment: Very good! Fixed. This is worth merging. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.10.2 Component: Compiler | Version: 7.8.4 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | typecheck/should_compile/T10195 Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-7.10`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC