Introduced new form of TcEvidence for KindCasts, this patch also fixes a
authorDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 22 Dec 2011 11:41:08 +0000 (11:41 +0000)
committerDimitrios Vytiniotis <dimitris@microsoft.com>
Thu, 22 Dec 2011 11:41:08 +0000 (11:41 +0000)
bug in zonking: we must zonk the kinds of existential variables even if
the variables themselves will not be affected.

compiler/deSugar/DsBinds.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcHsSyn.lhs

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