[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
              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