Introduced new form of TcEvidence for KindCasts, this patch also fixes a

bug in zonking: we must zonk the kinds of existential variables even if
the variables themselves will not be affected.

compiler/deSugar/DsBinds.lhs

@@ -683,7 +683,9 @@ dsEvTerm (EvId v) = Var v
 
 dsEvTerm (EvCast v co) 
   = dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-                                    -- unnecessary to call varToCoreExpr v here.
+                                     -- unnecessary to call varToCoreExpr v here.
+dsEvTerm (EvKindCast v co)
+  = dsTcCoercion co $ (\_ -> Var v)
 
 dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
 dsEvTerm (EvCoercion co)         = dsTcCoercion co mkEqBox

compiler/typecheck/TcEvidence.lhs

@@ -16,7 +16,7 @@ module TcEvidence (
 
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
 
-  EvTerm(..), mkEvCast, evVarsOfTerm,
+  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
 
   -- TcCoercion
   TcCoercion(..), 
@@ -447,27 +447,43 @@ evBindMapBinds bs
 data EvBind = EvBind EvVar EvTerm
 
 data EvTerm
-  = EvId EvId                  -- Term-level variable-to-variable bindings
-                               -- (no coercion variables! they come via EvCoercion)
+  = EvId EvId                    -- Term-level variable-to-variable bindings
+                                 -- (no coercion variables! they come via EvCoercion)
 
-  | EvCoercion TcCoercion      -- (Boxed) coercion bindings
+  | EvCoercion TcCoercion        -- (Boxed) coercion bindings
 
-  | EvCast EvVar TcCoercion    -- d |> co
+  | EvCast EvVar TcCoercion      -- d |> co
 
-  | EvDFunApp DFunId           -- Dictionary instance application
+  | EvDFunApp DFunId             -- Dictionary instance application
        [Type] [EvVar]
 
-  | EvTupleSel EvId  Int       -- n'th component of the tuple
+  | EvTupleSel EvId  Int         -- n'th component of the tuple
 
-  | EvTupleMk [EvId]           -- tuple built from this stuff
-
-  | EvSuperClass DictId Int    -- n'th superclass. Used for both equalities and
-                               -- dictionaries, even though the former have no
-                               -- selector Id.  We count up from _0_
+  | EvTupleMk [EvId]             -- tuple built from this stuff
 
+  | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and
+                                 -- dictionaries, even though the former have no
+                                 -- selector Id.  We count up from _0_
+  | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]
+           
   deriving( Data.Data, Data.Typeable)
 \end{code}
 
+Note [EvKindCast] 
+~~~~~~~~~~~~~~~~~ 
+
+EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 
+but the kinds of s1 and s2 (k1 and k2 respectively) don't match but 
+are rather equal by a coercion. You may think that this coercion will
+always turn out to be ReflCo, so why is this needed? Because sometimes
+we will want to defer kind errors until the runtime and in these cases
+that coercion will be an 'error' term, which we want to evaluate rather
+than silently forget about!
+
+The relevant (and only) place where such a coercion is produced in 
+the simplifier is in emit_kind_constraint in TcCanonical.
+
+
 Note [EvBinds/EvTerm]
 ~~~~~~~~~~~~~~~~~~~~~
 How evidence is created and updated. Bindings for dictionaries,
@@ -492,6 +508,11 @@ mkEvCast ev lco
   | isTcReflCo lco = EvId ev
   | otherwise      = EvCast ev lco
 
+mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
+mkEvKindCast ev lco
+  | isTcReflCo lco = EvId ev
+  | otherwise      = EvKindCast ev lco
+
 emptyTcEvBinds :: TcEvBinds
 emptyTcEvBinds = EvBinds emptyBag
 
@@ -508,6 +529,7 @@ evVarsOfTerm (EvTupleSel v _)    = [v]
 evVarsOfTerm (EvSuperClass v _)  = [v]
 evVarsOfTerm (EvCast v co)       = v : varSetElems (coVarsOfTcCo co)
 evVarsOfTerm (EvTupleMk evs)     = evs
+evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)
 \end{code}
 
 
@@ -561,6 +583,7 @@ instance Outputable EvBind where
 instance Outputable EvTerm where
   ppr (EvId v)           = ppr v
   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
+  ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs

compiler/typecheck/TcHsSyn.lhs

@@ -933,14 +933,23 @@ zonk_pat env (TuplePat pats boxed ty)
 	; (env', pats') <- zonkPats env pats
 	; return (env', TuplePat pats' boxed ty') }
 
-zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = evs, pat_binds = binds, pat_args = args })
-  = ASSERT( all isImmutableTyVar (pat_tvs p) ) 
+zonk_pat env p@(ConPatOut { pat_ty = ty, pat_tvs = tyvars
+                          , pat_dicts = evs, pat_binds = binds
+                          , pat_args = args })
+  = ASSERT( all isImmutableTyVar tyvars ) 
     do	{ new_ty <- zonkTcTypeToType env ty
-	; (env1, new_evs) <- zonkEvBndrsX env evs
+        ; (env0, new_tyvars) <- zonkTyBndrsX env tyvars
+          -- Must zonk the existential variables, because their
+          -- /kind/ need potential zonking.
+          -- cf typecheck/should_compile/tc221.hs
+	; (env1, new_evs) <- zonkEvBndrsX env0 evs
 	; (env2, new_binds) <- zonkTcEvBinds env1 binds
 	; (env', new_args) <- zonkConStuff env2 args
-	; returnM (env', p { pat_ty = new_ty, pat_dicts = new_evs, 
-			     pat_binds = new_binds, pat_args = new_args }) }
+	; returnM (env', p { pat_ty = new_ty, 
+                             pat_tvs = new_tyvars,
+                             pat_dicts = new_evs, 
+			     pat_binds = new_binds, 
+                             pat_args = new_args }) }
 
 zonk_pat env (LitPat lit) = return (env, LitPat lit)
 
@@ -1038,15 +1047,22 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
                              (varSetElemsKvsFirst unbound_tkvs)
                            ++ new_bndrs
 
-       ; return (HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs) }
+       ; return $ 
+         HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs }
   where
    zonk_bndr env (RuleBndr (L loc v)) 
-      = do { (env', v') <- zonk_it env v; return (env', RuleBndr (L loc v')) }
+      = do { (env', v') <- zonk_it env v
+           ; return (env', RuleBndr (L loc v')) }
    zonk_bndr _ (RuleBndrSig {}) = panic "zonk_bndr RuleBndrSig"
 
    zonk_it env v
-     | isId v     = do { v' <- zonkIdBndr env v; return (extendIdZonkEnv1 env v', v') }
-     | otherwise  = ASSERT( isImmutableTyVar v) return (env, v)
+     | isId v     = do { v' <- zonkIdBndr env v
+                       ; return (extendIdZonkEnv1 env v', v') }
+     | otherwise  = ASSERT( isImmutableTyVar v)
+                    zonkTyBndrX env v
+                    -- DV: used to be return (env,v) but that is plain 
+                    -- wrong because we may need to go inside the kind 
+                    -- of v and zonk there!
 \end{code}
 
 \begin{code}
@@ -1089,6 +1105,11 @@ zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
 zonkEvTerm env (EvCast v co)      = ASSERT( isId v) 
                                     do { co' <- zonkTcLCoToLCo env co
                                        ; return (mkEvCast (zonkIdOcc env v) co') }
+
+zonkEvTerm env (EvKindCast v co) = ASSERT( isId v) 
+                                    do { co' <- zonkTcLCoToLCo env co
+                                       ; return (mkEvKindCast (zonkIdOcc env v) co') }
+
 zonkEvTerm env (EvTupleSel v n)   = return (EvTupleSel (zonkIdOcc env v) n)
 zonkEvTerm env (EvTupleMk vs)     = return (EvTupleMk (map (zonkIdOcc env) vs))
 zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n)