Further improvements to floating equalities

This equality-floating stuff is horribly delicate!  Trac #9316 showed
up yet another corner case.

The main changes are
 * include CTyVarEqs when "growing" the skolem set
 * do not include the kind argument to (~) when growing the skolem set

I added a lot more comments as well

3 files changed, 279 insertions, 120 deletions

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 843e0507dc..dde5902ccc 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -843,39 +843,6 @@ Consider floated_eqs (all wanted or derived):
     simpl_loop.  So we iterate if there any of these
 
 \begin{code}
-floatEqualities :: [TcTyVar] -> Bool -> WantedConstraints
-                -> TcS (Cts, WantedConstraints)
--- Post: The returned floated constraints (Cts) are only Wanted or Derived
--- and come from the input wanted ev vars or deriveds
--- Also performs some unifications, adding to monadically-carried ty_binds
--- These will be used when processing floated_eqs later
-floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
-  | not no_given_eqs  -- There are some given equalities, so don't float
-  = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
-  | otherwise
-  = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
-       ; untch <- TcS.getUntouchables
-       ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
-             -- See Note [Promoting unification variables]
-       ; ty_binds <- getTcSTyBindsMap
-       ; traceTcS "floatEqualities" (vcat [ text "Flats =" <+> ppr flats
-                                          , text "Floated eqs =" <+> ppr float_eqs
-                                          , text "Ty binds =" <+> ppr ty_binds])
-       ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
-  where
-      -- See Note [Float equalities from under a skolem binding]
-    skol_set = fixVarSet mk_next (mkVarSet skols)
-    mk_next tvs = foldrBag grow_one tvs flats
-    grow_one (CFunEqCan { cc_tyargs = xis, cc_rhs = rhs }) tvs
-       | intersectsVarSet tvs (tyVarsOfTypes xis)
-       = tvs `unionVarSet` tyVarsOfType rhs
-    grow_one _ tvs = tvs
-
-    is_floatable :: Ct -> Bool
-    is_floatable ct = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
-       where
-         pred = ctPred ct
-
 promoteTyVar :: Untouchables -> TcTyVar  -> TcS ()
 -- When we float a constraint out of an implication we must restore
 -- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
@@ -1036,6 +1003,80 @@ should!  If we don't solve the constraint, we'll stupidly quantify over
 (b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
 Trac #7641 is a simpler example.
 
+Note [Promoting unification variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we float an equality out of an implication we must "promote" free
+unification variables of the equality, in order to maintain Invariant
+(MetaTvInv) from Note [Untouchable type variables] in TcType.  for the
+leftover implication.
+
+This is absolutely necessary. Consider the following example. We start
+with two implications and a class with a functional dependency.
+
+    class C x y | x -> y
+    instance C [a] [a]
+
+    (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
+    (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
+
+We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
+They may react to yield that (beta := [alpha]) which can then be pushed inwards
+the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
+(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
+beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
+
+    class C x y | x -> y where
+     op :: x -> y -> ()
+
+    instance C [a] [a]
+
+    type family F a :: *
+
+    h :: F Int -> ()
+    h = undefined
+
+    data TEx where
+      TEx :: a -> TEx
+
+
+    f (x::beta) =
+        let g1 :: forall b. b -> ()
+            g1 _ = h [x]
+            g2 z = case z of TEx y -> (h [[undefined]], op x [y])
+        in (g1 '3', g2 undefined)
+
+
+
+Note [Solving Family Equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+After we are done with simplification we may be left with constraints of the form:
+     [Wanted] F xis ~ beta
+If 'beta' is a touchable unification variable not already bound in the TyBinds
+then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
+
+When is it ok to do so?
+    1) 'beta' must not already be defaulted to something. Example:
+
+           [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
+           [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We
+                                       have to report this as unsolved.
+
+    2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
+       set [beta := F xis] only if beta is not among the free variables of xis.
+
+    3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
+       of type family equations. See Inert Set invariants in TcInteract.
+
+This solving is now happening during zonking, see Note [Unflattening while zonking]
+in TcMType.
+
+
+*********************************************************************************
+*                                                                               *
+*                          Floating equalities                                  *
+*                                                                               *
+*********************************************************************************
+
 Note [Float Equalities out of Implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For ordinary pattern matches (including existentials) we float
@@ -1081,8 +1122,59 @@ Consequence: classes with functional dependencies don't matter (since there is
 no evidence for a fundep equality), but equality superclasses do matter (since
 they carry evidence).
 
+\begin{code}
+floatEqualities :: [TcTyVar] -> Bool -> WantedConstraints
+                -> TcS (Cts, WantedConstraints)
+-- Main idea: see Note [Float Equalities out of Implications]
+--
+-- Post: The returned floated constraints (Cts) are only Wanted or Derived
+-- and come from the input wanted ev vars or deriveds
+-- Also performs some unifications (via promoteTyVar), adding to
+-- monadically-carried ty_binds. These will be used when processing 
+-- floated_eqs later
+--
+-- Subtleties: Note [Float equalities from under a skolem binding]
+--             Note [Skolem escape]
+floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats })
+  | not no_given_eqs  -- There are some given equalities, so don't float
+  = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+  | otherwise
+  = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
+       ; untch <- TcS.getUntouchables
+       ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
+             -- See Note [Promoting unification variables]
+       ; ty_binds <- getTcSTyBindsMap
+       ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
+                                          , text "Flats =" <+> ppr flats
+                                          , text "Skol set =" <+> ppr skol_set
+                                          , text "Floated eqs =" <+> ppr float_eqs
+                                          , text "Ty binds =" <+> ppr ty_binds])
+       ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
+  where
+    is_floatable :: Ct -> Bool
+    is_floatable ct
+       = case classifyPredType (ctPred ct) of
+            EqPred ty1 ty2 -> skol_set `disjointVarSet` tyVarsOfType ty1
+                           && skol_set `disjointVarSet` tyVarsOfType ty2
+            _ -> False
+
+    skol_set = fixVarSet mk_next (mkVarSet skols)
+    mk_next tvs = foldr grow_one tvs flat_eqs
+    flat_eqs :: [(TcTyVarSet, TcTyVarSet)]
+    flat_eqs = [ (tyVarsOfType ty1, tyVarsOfType ty2)
+               | EqPred ty1 ty2 <- map (classifyPredType . ctPred) (bagToList flats)]
+    grow_one (tvs1,tvs2) tvs
+      | intersectsVarSet tvs tvs1 = tvs `unionVarSet` tvs2
+      | intersectsVarSet tvs tvs2 = tvs `unionVarSet` tvs2
+      | otherwise                 = tvs
+\end{code}
+
 Note [When does an implication have given equalities?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+     NB: This note is mainly referred to from TcSMonad
+         but it relates to floating equalities, so I've
+         left it here
+
 Consider an implication
    beta => alpha ~ Int
 where beta is a unification variable that has already been unified
@@ -1126,116 +1218,95 @@ This seems like the Right Thing, but it's more code, and more work
 at runtime, so we are using the FlatSkolOrigin idea intead. It's less
 obvious that it works, but I think it does, and it's simple and efficient.
 
-
 Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-You might worry about skolem escape with all this floating.
-For example, consider
-    [2] forall a. (a ~ F beta[2] delta,
-                   Maybe beta[2] ~ gamma[1])
-
-The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
-solve with gamma := beta. But what if later delta:=Int, and
-  F b Int = b.
-Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
-skolem has escaped!
-
-But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
-to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
-
-Previously we tried to "grow" the skol_set with the constraints, to get
-all the tyvars that could *conceivably* unify with the skolems, but that
-was far too conservative (Trac #7804). Example: this should be fine:
-    f :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
-    f = error "Urk" :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
-
-BUT (sigh) we have to be careful.  Here are some edge cases:
+Which of the flat equalities can we float out?  Obviously, only
+ones that don't mention the skolem-bound variables.  But that is
+over-eager. Consider
+   [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
+The second constraint doesn't mention 'a'.  But if we float it
+we'll promote gamma to gamma'[1].  Now suppose that we learn that
+beta := Bool, and F a Bool = a, and G Bool _ = Int.  Then we'll
+we left with the constraint
+   [2] forall a. a ~ gamma'[1]
+which is insoluble because gamma became untouchable.
+
+Solution: only promote a constraint if its free variables cannot
+possibly be connected with the skolems.  Procedurally, start with
+the skolems and "grow" that set as follows:
+  * For each flat equality F ts ~ s, or tv ~ s,
+    if the current set intersects with the LHS of the equality,
+       add the free vars of the RHS, and vice versa
+That gives us a grown skolem set.  Now float an equality if its free
+vars don't intersect the grown skolem set.
+
+This seems very ad hoc (sigh).  But here are some tricky edge cases:
 
 a)    [2]forall a. (F a delta[1] ~ beta[2],   delta[1] ~ Maybe beta[2])
-b)    [2]forall a. (F b ty ~ beta[2],         G beta[2] ~ gamma[2])
+b1)   [2]forall a. (F a ty ~ beta[2],         G beta[2] ~ gamma[2])
+b2)   [2]forall a. (a ~ beta[2],              G beta[2] ~ gamma[2])
 c)    [2]forall a. (F a ty ~ beta[2],         delta[1] ~ Maybe beta[2])
+d)    [2]forall a. (gamma[1] ~ Tree beta[2],  F ty ~ beta[2])
 
 In (a) we *must* float out the second equality,
        else we can't solve at all (Trac #7804).
 
-In (b) we *must not* float out the second equality.
-       It will ultimately be solved (by flattening) in situ, but if we
-       float it we'll promote beta,gamma, and render the first equality insoluble.
+In (b1, b2) we *must not* float out the second equality.
+       It will ultimately be solved (by flattening) in situ, but if we float
+       it we'll promote beta,gamma, and render the first equality insoluble.
+
+       Trac #9316 was an example of (b2).  You may wonder why (a ~ beta[2]) isn't
+       solved; in #9316 it wasn't solved because (a:*) and (beta:kappa[1]), so the
+       equality was kind-mismatched, and hence was a CIrredEvCan.  There was
+       another equality alongside, (kappa[1] ~ *).  We must first float *that*
+       one out and *then* we can solve (a ~ beta).
 
 In (c) it would be OK to float the second equality but better not to.
        If we flatten we see (delta[1] ~ Maybe (F a ty)), which is a
-       skolem-escape problem.  If we float the secodn equality we'll
+       skolem-escape problem.  If we float the second equality we'll
        end up with (F a ty ~ beta'[1]), which is a less explicable error.
 
-Hence we start with the skolems, grow them by the CFunEqCans, and
-float ones that don't mention the grown variables.  Seems very ad hoc.
-
-Note [Promoting unification variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we float an equality out of an implication we must "promote" free
-unification variables of the equality, in order to maintain Invariant
-(MetaTvInv) from Note [Untouchable type variables] in TcType.  for the
-leftover implication.
-
-This is absolutely necessary. Consider the following example. We start
-with two implications and a class with a functional dependency.
-
-    class C x y | x -> y
-    instance C [a] [a]
-
-    (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
-    (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
-
-We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
-They may react to yield that (beta := [alpha]) which can then be pushed inwards
-the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
-(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
-beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
-
-    class C x y | x -> y where
-     op :: x -> y -> ()
-
-    instance C [a] [a]
-
-    type family F a :: *
-
-    h :: F Int -> ()
-    h = undefined
-
-    data TEx where
-      TEx :: a -> TEx
+In (d) we must float the first equality, so that we can unify gamma.
+       But that promotes beta, so we must float the second equality too,
+       Trac #7196 exhibits this case
 
+Some notes
 
-    f (x::beta) =
-        let g1 :: forall b. b -> ()
-            g1 _ = h [x]
-            g2 z = case z of TEx y -> (h [[undefined]], op x [y])
-        in (g1 '3', g2 undefined)
+* When "growing", do not simply take the free vars of the predicate!
+  Example    [2]forall a.  (a:* ~ beta[2]:kappa[1]), (kappa[1] ~ *)
+  We must float the second, and we must not float the first.
+  But the first actually looks like ((~) kappa a beta), so if we just
+  look at its free variables we'll see {a,kappa,beta), and that might
+  make us think kappa should be in the grown skol set.
 
+  (In any case, the kind argument for a kind-mis-matched equality like
+   this one doesn't really make sense anyway.)
 
+  That's why we use classifyPred when growing.
 
-Note [Solving Family Equations]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-After we are done with simplification we may be left with constraints of the form:
-     [Wanted] F xis ~ beta
-If 'beta' is a touchable unification variable not already bound in the TyBinds
-then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
-
-When is it ok to do so?
-    1) 'beta' must not already be defaulted to something. Example:
+* Previously we tried to "grow" the skol_set with *all* the
+  constraints (not just equalities), to get all the tyvars that could
+  *conceivably* unify with the skolems, but that was far too
+  conservative (Trac #7804). Example: this should be fine:
+    f :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
+    f = error "Urk" :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
 
-           [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
-           [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We
-                                       have to report this as unsolved.
 
-    2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
-       set [beta := F xis] only if beta is not among the free variables of xis.
+Note [Skolem escape]
+~~~~~~~~~~~~~~~~~~~~
+You might worry about skolem escape with all this floating.
+For example, consider
+    [2] forall a. (a ~ F beta[2] delta,
+                   Maybe beta[2] ~ gamma[1])
 
-    3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
-       of type family equations. See Inert Set invariants in TcInteract.
+The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
+solve with gamma := beta. But what if later delta:=Int, and
+  F b Int = b.
+Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
+skolem has escaped!
 
-This solving is now happening during zonking, see Note [Unflattening while zonking]
-in TcMType.
+But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
+to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
 
 
 *********************************************************************************
diff --git a/testsuite/tests/indexed-types/should_compile/T9316.hs b/testsuite/tests/indexed-types/should_compile/T9316.hs
new file mode 100644
index 0000000000..b5dfca6a94
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T9316.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module SingletonsBug where
+
+import Control.Applicative
+import Data.Traversable (for)
+import GHC.Exts( Constraint )
+
+-----------------------------------
+-- From 'constraints' library
+-- import Data.Constraint (Dict(..))
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+-----------------------------------
+-- From 'singletons' library
+-- import Data.Singletons hiding( withSomeSing )
+
+class SingI (a :: k) where
+  -- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
+  -- extension to use this method the way you want.
+  sing :: Sing a
+
+data family Sing (a :: k)
+
+data KProxy (a :: *) = KProxy
+
+data SomeSing (kproxy :: KProxy k) where
+  SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
+
+-- SingKind :: forall k. KProxy k -> Constraint
+class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
+  -- | Get a base type from a proxy for the promoted kind. For example,
+  -- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
+  type DemoteRep kparam :: *
+
+  -- | Convert a singleton to its unrefined version.
+  fromSing :: Sing (a :: k) -> DemoteRep kparam
+
+  -- | Convert an unrefined type to an existentially-quantified singleton type.
+  toSing   :: DemoteRep kparam -> SomeSing kparam
+
+withSomeSing :: SingKind ('KProxy :: KProxy k)
+             => DemoteRep ('KProxy :: KProxy k)
+             -> (forall (a :: k). Sing a -> r)
+             -> r
+withSomeSing = error "urk"
+
+-----------------------------------
+
+data SubscriptionChannel = BookingsChannel
+type BookingsChannelSym0 = BookingsChannel
+data instance Sing (z_a5I7 :: SubscriptionChannel) where
+   SBookingsChannel :: Sing BookingsChannel
+
+instance SingKind ('KProxy :: KProxy SubscriptionChannel) where
+  type DemoteRep ('KProxy :: KProxy SubscriptionChannel) = SubscriptionChannel
+  fromSing SBookingsChannel = BookingsChannel
+  toSing BookingsChannel = SomeSing SBookingsChannel
+
+instance SingI BookingsChannel where
+  sing = SBookingsChannel
+
+type family T (c :: SubscriptionChannel) :: *
+type instance T 'BookingsChannel = Bool
+
+witnessC :: Sing channel -> Dict (Show (T channel), SingI channel)
+witnessC SBookingsChannel = Dict
+
+forAllSubscriptionChannels
+  :: forall m r. (Applicative m)
+  => (forall channel. (SingI channel, Show (T channel)) => Sing channel -> m r)
+  -> m r
+forAllSubscriptionChannels f =
+  withSomeSing BookingsChannel $ \(sChannel) ->
+    case witnessC sChannel of
+      Dict -> f sChannel
+
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 7c41be8afb..016444a138 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -244,3 +244,4 @@ test('T8913', normal, compile, [''])
 test('T8978', normal, compile, [''])
 test('T8979', normal, compile, [''])
 test('T9085', normal, compile, [''])
+test('T9316', normal, compile, [''])