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.

3 files changed, 68 insertions, 22 deletions

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index d44943c347..7cc58583dd 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/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
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 0511aa1051..87aaa3238d 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/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

diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index eca79984af..3e18da52cc 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/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)