#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