GHC forgets constraints when matching on GADTs

Here's a relatively short piece of code that doesn't compile:

{-# 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 ofmagic 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.)

1. 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.

1. 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?
2. 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.
3. Add PolyKinds. Not sure why this would affect anything.
4. Change the signature of fromScalar to r -> s. Not sure why this would affect anything.