[GHC] #10195: GHC forgets constraints when matching on GADTs

[GHC]

#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