Do not generate given kind-equalities (fix Trac #8566)

This is a long-standing bug.  We were generating a Given
equality between kind variables, and (at least until we support
kind coercions) we can't do that.

The fix is to drop such Given equalities entirely. That may
mean we can't prove some things, but that's fair enough -- the
current proof language can't express such proofs.

See Note [Do not create Given kind equalities] in TcSMonad

3 files changed, 77 insertions, 40 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 6f8e3db228..2e90745533 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -208,7 +208,7 @@ canTuple ev tys
   = do { traceTcS "can_pred" (text "TuplePred!")
        ; let xcomp = EvTupleMk
              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
-       ; ctevs <- xCtFlavor ev tys (XEvTerm xcomp xdecomp)
+       ; ctevs <- xCtFlavor ev (XEvTerm tys xcomp xdecomp)
        ; canEvVarsCreated ctevs }
 \end{code}
 
@@ -332,9 +332,10 @@ newSCWorkFromFlavored flavor cls xis
   | isGiven flavor
   = do { let sc_theta = immSuperClasses cls xis
              xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..]
-             xev = XEvTerm { ev_comp   = panic "Can't compose for given!"
+             xev = XEvTerm { ev_preds  =  sc_theta
+                           , ev_comp   = panic "Can't compose for given!"
                            , ev_decomp = xev_decomp }
-       ; ctevs <- xCtFlavor flavor sc_theta xev
+       ; ctevs <- xCtFlavor flavor xev
        ; emitWorkNC ctevs }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
@@ -784,7 +785,7 @@ canEqNC ev ty1 ty2
                  xevdecomp x = let xco = evTermCoercion x
                                in [ EvCoercion (mkTcLRCo CLeft xco)
                                   , EvCoercion (mkTcLRCo CRight xco)]
-           ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
+           ; ctevs <- xCtFlavor ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
            ; canEvVarsCreated ctevs }
 
       | otherwise
@@ -803,8 +804,8 @@ canDecomposableTyConApp ev tc1 tys1 tc2 tys2
   | otherwise
   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
-             xev = XEvTerm xcomp xdecomp
-       ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
+             xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
+       ; ctevs <- xCtFlavor ev xev
        ; canEvVarsCreated ctevs }
 
 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue
@@ -1051,8 +1052,8 @@ canEqLeaf ev s1 s2
        ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
              xcomp _ = panic "canEqLeaf: can't happen"
              xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
-             xev = XEvTerm xcomp xdecomp
-       ; ctevs <- xCtFlavor ev [mkTcEqPred s2 s1] xev
+             xev = XEvTerm [mkTcEqPred s2 s1] xcomp xdecomp
+       ; ctevs <- xCtFlavor ev xev
        ; case ctevs of
            []     -> return Stop
            [ctev] -> canEqLeafOriented ctev cls2 s1
@@ -1108,7 +1109,8 @@ canEqLeafTyVar ev tv s2              -- ev :: tv ~ s2
        ; let co = mkHdEqPred s2 co1 co2
              -- co :: (xi1 ~ xi2) ~ (tv ~ s2)
 
-       ; traceTcS "canEqLeafTyVar 2" $ vcat [ppr xi1, ppr xi2]
+       ; traceTcS "canEqLeafTyVar 2" $ vcat [ ppr xi1 <+> dcolon <+> ppr (typeKind xi1)
+                                            , ppr xi2 <+> dcolon <+> ppr (typeKind xi2)]
        ; case (getTyVar_maybe xi1, getTyVar_maybe xi2) of
            (Nothing,  _) -> -- Rewriting the LHS did not yield a type variable
                             -- so go around again to canEq
@@ -1164,22 +1166,20 @@ checkKind :: CtEvidence          -- t1~t2
 -- for the type equality; and continue with the kind equality constraint.
 -- When the latter is solved, it'll kick out the irreducible equality for
 -- a second attempt at solving
--- See Note [Equalities with incompatible kinds]
 
-checkKind new_ev s1 s2
+checkKind new_ev s1 s2   -- See Note [Equalities with incompatible kinds]
   = ASSERT( isKind k1 && isKind k2 )
-    do {  -- See Note [Equalities with incompatible kinds]
-         traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
+    do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
+
+         -- Put the not-currently-soluble thing back onto the work list
        ; updWorkListTcS $ extendWorkListNonEq $
          CIrredEvCan { cc_ev = new_ev }
+
+         -- Create a derived kind-equality, and solve it
        ; mw <- newDerived kind_co_loc (mkEqPred k1 k2)
        ; case mw of
            Nothing  -> return Stop
            Just kev -> canEqNC kev k1 k2 }
-
-         -- Always create a Wanted kind equality even if
-         -- you are decomposing a given constraint.
-         -- NB: DV finds this reasonable for now. Maybe we have to revisit.
   where
     k1 = typeKind s1
     k2 = typeKind s2
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 432388822e..2056561336 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -553,7 +553,7 @@ solveFunEq :: CtEvidence    -- From this  :: F tys ~ xi1
            -> Type
            -> TcS ()
 solveFunEq from_this xi1 solve_this xi2
-  = do { ctevs <- xCtFlavor solve_this [mkTcEqPred xi2 xi1] xev
+  = do { ctevs <- xCtFlavor solve_this xev
              -- No caching!  See Note [Cache-caused loops]
              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 
@@ -561,7 +561,7 @@ solveFunEq from_this xi1 solve_this xi2
   where
     from_this_co = evTermCoercion $ ctEvTerm from_this
 
-    xev = XEvTerm xcomp xdecomp
+    xev = XEvTerm [mkTcEqPred xi2 xi1] xcomp xdecomp
 
     -- xcomp : [(xi2 ~ xi1)] -> (F tys ~ xi2)
     xcomp [x] = EvCoercion (from_this_co `mkTcTransCo` mk_sym_co x)
@@ -694,6 +694,9 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev
               -> do { untch <- getUntouchables
                     ; traceTcS "Can't solve tyvar equality"
                           (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+                                , ppWhen (isMetaTyVar tv) $
+                                  nest 4 (text "Untouchable level of" <+> ppr tv
+                                          <+> text "is" <+> ppr (metaTyVarUntouchables tv))
                                 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
                                 , text "Untouchables =" <+> ppr untch ])
                     ; (n_kicked, inerts') <- kickOutRewritable ev tv inerts
@@ -1514,7 +1517,7 @@ doTopReactFunEq _ct fl fun_tc args xi
 
     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
-      = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
+      = do { ctevs <- xCtFlavor fl xev
            ; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
            ; case ctevs of
                [ctev] -> updWorkListTcS $ extendWorkListEq $
@@ -1527,7 +1530,7 @@ doTopReactFunEq _ct fl fun_tc args xi
         xdecomp x = [EvCoercion (mkTcSymCo co `mkTcTransCo` evTermCoercion x)]
         xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
         xcomp _   = panic "No more goals!"
-        xev = XEvTerm xcomp xdecomp
+        xev = XEvTerm [mkTcEqPred rhs_ty xi] xcomp xdecomp
 \end{code}
 
 Note [Cached solved FunEqs]
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 78ecea18ac..f265f5fb5a 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -135,7 +135,7 @@ import Maybes ( orElse, catMaybes, firstJust )
 import Pair ( pSnd )
 
 import TrieMap
-import Control.Monad( ap, when, zipWithM )
+import Control.Monad( ap, when )
 import Data.IORef
 import Data.List( partition )
 
@@ -1504,12 +1504,11 @@ instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
 -- Creating and setting evidence variables and CtFlavors
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-data XEvTerm =
-  XEvTerm { ev_comp   :: [EvTerm] -> EvTerm
-                         -- How to compose evidence
-          , ev_decomp :: EvTerm -> [EvTerm]
-                         -- How to decompose evidence
-          }
+data XEvTerm
+  = XEvTerm { ev_preds  :: [PredType]           -- New predicate types
+            , ev_comp   :: [EvTerm] -> EvTerm   -- How to compose evidence
+            , ev_decomp :: EvTerm -> [EvTerm]   -- How to decompose evidence
+            }
 
 data MaybeNew = Fresh CtEvidence | Cached EvTerm
 
@@ -1538,11 +1537,11 @@ setEvBind the_ev tm
        ; tc_evbinds <- getTcEvBinds
        ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
 
-newGivenEvVar :: CtLoc -> TcPredType -> EvTerm -> TcS CtEvidence
+newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
-newGivenEvVar loc pred rhs
+newGivenEvVar loc (pred, rhs)
   = do { new_ev <- wrapTcS $ TcM.newEvVar pred
        ; setEvBind new_ev rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
@@ -1553,7 +1552,7 @@ newWantedEvVarNC loc pty
   = do { new_ev <- wrapTcS $ TcM.newEvVar pty
        ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
 
--- | Variant of newGivenEvVar that has a lower bound on the depth of the result
+-- | Variant of newWantedEvVar that has a lower bound on the depth of the result
 --   (see Note [Preventing recursive dictionaries])
 newWantedEvVarNonrec :: CtLoc -> TcPredType -> TcS MaybeNew
 newWantedEvVarNonrec loc pty
@@ -1629,24 +1628,59 @@ But that superclass selector can't (yet) appear in a coercion
 
 See Note [Coercion evidence terms] in TcEvidence.
 
+Note [Do not create Given kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do not want to create a Given like
+
+     kv ~ k            -- kv is a skolem kind variable
+                       -- Reason we don't yet support non-Refl kind equalities
+
+or   t1::k1 ~ t2::k2   -- k1 and k2 are un-equal kinds
+                       -- Reason: (~) is kind-uniform at the moment, and
+                       -- k1/k2 may be distinct kind skolems
+
+This showed up in Trac #8566, where we had a data type
+   data I (u :: U *) (r :: [*]) :: * where
+        A :: I (AA t as) r                  -- Existential k
+so A has type
+   A :: forall (u:U *) (r:[*])                  Universal
+        (k:BOX) (t:k) (as:[U *]).        Existential
+        (u ~ AA * k t as) => I u r
+
+There is no direct kind equality, but in a pattern match where 'u' is
+instantiated to, say, (AA * kk t1 as1), we'd decompose to get
+   k ~ kk, t ~ t1, as ~ as1
+This is bad.  We "fix" this by simply ignoring
+  *     the Given kind equality
+  * AND the Given type equality (t:k1) ~ (t1:kk)
+
 
 \begin{code}
 xCtFlavor :: CtEvidence            -- Original flavor
-          -> [TcPredType]          -- New predicate types
           -> XEvTerm               -- Instructions about how to manipulate evidence
           -> TcS [CtEvidence]
 
-xCtFlavor (CtGiven { ctev_evtm = tm, ctev_loc = loc }) ptys xev
-  = ASSERT( equalLength ptys (ev_decomp xev tm) )
-    zipWithM (newGivenEvVar loc) ptys (ev_decomp xev tm)
-    -- See Note [Bind new Givens immediately]
+xCtFlavor (CtGiven { ctev_evtm = tm, ctev_loc = loc })
+          (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
+  = ASSERT( equalLength ptys (decomp_fn tm) )
+    mapM (newGivenEvVar loc)     -- See Note [Bind new Givens immediately]
+         (filterOut bad_given_pred (ptys `zip` decomp_fn tm))
+  where
+    -- See Note [Do not create Given kind equalities]
+    bad_given_pred (pred_ty, _)
+      | EqPred t1 t2 <- classifyPredType pred_ty
+      = isKind t1 || not (typeKind t1 `tcEqKind` typeKind t2)
+      | otherwise
+      = False
 
-xCtFlavor (CtWanted { ctev_evar = evar, ctev_loc = loc }) ptys xev
+xCtFlavor (CtWanted { ctev_evar = evar, ctev_loc = loc })
+          (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
   = do { new_evars <- mapM (newWantedEvVar loc) ptys
-       ; setEvBind evar (ev_comp xev (getEvTerms new_evars))
+       ; setEvBind evar (comp_fn (getEvTerms new_evars))
        ; return (freshGoals new_evars) }
 
-xCtFlavor (CtDerived { ctev_loc = loc }) ptys _xev
+xCtFlavor (CtDerived { ctev_loc = loc })
+          (XEvTerm { ev_preds = ptys })
   = do { ders <- mapM (newDerived loc) ptys
        ; return (catMaybes ders) }
 
@@ -1700,7 +1734,7 @@ rewriteCtFlavor old_ev new_pred co
        -- then retain the old type, so that error messages come out mentioning synonyms
 
 rewriteCtFlavor (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
-  = do { new_ev <- newGivenEvVar loc new_pred new_tm  -- See Note [Bind new Givens immediately]
+  = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
        ; return (Just new_ev) }
   where
     new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo