Add a provenance field to universal coercions.
authorIavor S. Diatchki <diatchki@galois.com>
Thu, 18 Dec 2014 02:46:36 +0000 (18:46 -0800)
committerIavor S. Diatchki <diatchki@galois.com>
Thu, 18 Dec 2014 02:46:36 +0000 (18:46 -0800)
Universal coercions allow casting between arbitrary types, so it is a
good idea to keep track where they came from, which now we can do by
using the provenance field in `UnivCo`.

This is also handy for type-checker plugins that provide functionality
beyond what's expressible by GHC's standard coercions:  such plugins
can generate universal coercions, but they should still tag them,
so that if something goes wrong we can link the casts to the plugin.

compiler/coreSyn/CoreLint.hs
compiler/coreSyn/TrieMap.hs
compiler/deSugar/DsBinds.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/iface/TcIface.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcType.hs
compiler/types/Coercion.hs
compiler/types/OptCoercion.hs

index 7c636b4..3dca78e 100644 (file)
@@ -1124,7 +1124,7 @@ lintCoercion (CoVarCo cv)
                                      2 (ppr cv)) }
        ; return (k, s, t, r) }
 
-lintCoercion (UnivCo r ty1 ty2)
+lintCoercion (UnivCo _prov r ty1 ty2)
   = do { k1 <- lintType ty1
        ; _k2 <- lintType ty2
 --       ; unless (k1 `eqKind` k2) $
index aa9172b..efae286 100644 (file)
@@ -528,7 +528,9 @@ lkC env co m
     go (AxiomInstCo ax ind cs) = km_axiom  >.> lkNamed ax >=> lookupTM ind >=> lkList (lkC env) cs
     go (AppCo c1 c2)           = km_app    >.> lkC env c1 >=> lkC env c2
     go (TransCo c1 c2)         = km_trans  >.> lkC env c1 >=> lkC env c2
-    go (UnivCo r t1 t2)        = km_univ   >.> lookupTM r >=> lkT env t1 >=> lkT env t2
+
+    -- the provenance is not used in the map
+    go (UnivCo _ r t1 t2)      = km_univ   >.> lookupTM r >=> lkT env t1 >=> lkT env t2
     go (InstCo c t)            = km_inst   >.> lkC env c  >=> lkT env t
     go (ForAllCo v c)          = km_forall >.> lkC (extendCME env v) c >=> lkBndr env v
     go (CoVarCo v)             = km_var    >.> lkVar env v
@@ -550,7 +552,8 @@ xtC env (TyConAppCo r tc cs)    f m = m { km_tc_app = km_tc_app m |> xtR r |>> x
 xtC env (AxiomInstCo ax ind cs) f m = m { km_axiom  = km_axiom m  |> xtNamed ax |>> xtInt ind |>> xtList (xtC env) cs f }
 xtC env (AppCo c1 c2)           f m = m { km_app    = km_app m    |> xtC env c1 |>> xtC env c2 f }
 xtC env (TransCo c1 c2)         f m = m { km_trans  = km_trans m  |> xtC env c1 |>> xtC env c2 f }
-xtC env (UnivCo r t1 t2)        f m = m { km_univ   = km_univ   m |> xtR r |>> xtT env t1 |>> xtT env t2 f }
+-- the provenance is not used in the map
+xtC env (UnivCo _ r t1 t2)        f m = m { km_univ   = km_univ   m |> xtR r |>> xtT env t1 |>> xtT env t2 f }
 xtC env (InstCo c t)            f m = m { km_inst   = km_inst m   |> xtC env c  |>> xtT env t  f }
 xtC env (ForAllCo v c)          f m = m { km_forall = km_forall m |> xtC (extendCME env v) c
                                                       |>> xtBndr env v f }
index f328ce9..b512fbb 100644 (file)
@@ -957,7 +957,7 @@ ds_tc_coercion subst tc_co
                                 (subst', tv') = Coercion.substTyVarBndr subst tv
     go (TcAxiomInstCo ax ind cos)
                                 = AxiomInstCo ax ind (map go cos)
-    go (TcPhantomCo ty1 ty2)    = UnivCo Phantom ty1 ty2
+    go (TcPhantomCo ty1 ty2)    = UnivCo (fsLit "ds_tc_coercion") Phantom ty1 ty2
     go (TcSymCo co)             = mkSymCo (go co)
     go (TcTransCo co1 co2)      = mkTransCo (go co1) (go co2)
     go (TcNthCo n co)           = mkNthCo n (go co)
index d850f66..ead3da4 100644 (file)
@@ -1152,7 +1152,7 @@ freeNamesIfCoercion (IfaceCoVarCo _)
   = emptyNameSet
 freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
   = unitNameSet ax &&& fnList freeNamesIfCoercion cos
-freeNamesIfCoercion (IfaceUnivCo _ t1 t2)
+freeNamesIfCoercion (IfaceUnivCo _ t1 t2)
   = freeNamesIfType t1 &&& freeNamesIfType t2
 freeNamesIfCoercion (IfaceSymCo c)
   = freeNamesIfCoercion c
index 5345453..b20e674 100644 (file)
@@ -141,7 +141,7 @@ data IfaceCoercion
   | IfaceForAllCo    IfaceTvBndr IfaceCoercion
   | IfaceCoVarCo     IfLclName
   | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
-  | IfaceUnivCo      Role IfaceType IfaceType
+  | IfaceUnivCo      FastString Role IfaceType IfaceType
   | IfaceSymCo       IfaceCoercion
   | IfaceTransCo     IfaceCoercion IfaceCoercion
   | IfaceNthCo       Int IfaceCoercion
@@ -593,9 +593,9 @@ ppr_co ctxt_prec co@(IfaceForAllCo _ _)
 
 ppr_co _         (IfaceCoVarCo covar)       = ppr covar
 
-ppr_co ctxt_prec (IfaceUnivCo r ty1 ty2)
+ppr_co ctxt_prec (IfaceUnivCo r ty1 ty2)
   = maybeParen ctxt_prec TyConPrec $
-    ptext (sLit "UnivCo") <+> ppr r <+>
+    ptext (sLit "UnivCo") <+> ftext s <+> ppr r <+>
     pprParendIfaceType ty1 <+> pprParendIfaceType ty2
 
 ppr_co ctxt_prec (IfaceInstCo co ty)
@@ -788,11 +788,12 @@ instance Binary IfaceCoercion where
           put_ bh a
           put_ bh b
           put_ bh c
-  put_ bh (IfaceUnivCo a b c) = do
+  put_ bh (IfaceUnivCo a b c d) = do
           putByte bh 8
           put_ bh a
           put_ bh b
           put_ bh c
+          put_ bh d
   put_ bh (IfaceSymCo a) = do
           putByte bh 9
           put_ bh a
@@ -850,7 +851,8 @@ instance Binary IfaceCoercion where
            8 -> do a <- get bh
                    b <- get bh
                    c <- get bh
-                   return $ IfaceUnivCo a b c
+                   d <- get bh
+                   return $ IfaceUnivCo a b c d
            9 -> do a <- get bh
                    return $ IfaceSymCo a
            10-> do a <- get bh
@@ -954,7 +956,7 @@ toIfaceCoercion (CoVarCo cv)        = IfaceCoVarCo  (toIfaceCoVar cv)
 toIfaceCoercion (AxiomInstCo con ind cos)
                                     = IfaceAxiomInstCo (coAxiomName con) ind
                                                        (map toIfaceCoercion cos)
-toIfaceCoercion (UnivCo r ty1 ty2)  = IfaceUnivCo r (toIfaceType ty1)
+toIfaceCoercion (UnivCo s r ty1 ty2)= IfaceUnivCo s r (toIfaceType ty1)
                                                   (toIfaceType ty2)
 toIfaceCoercion (SymCo co)          = IfaceSymCo (toIfaceCoercion co)
 toIfaceCoercion (TransCo co1 co2)   = IfaceTransCo (toIfaceCoercion co1)
index cf0dc5b..4c0440f 100644 (file)
@@ -880,7 +880,7 @@ tcIfaceCo (IfaceCoVarCo n)          = mkCoVarCo <$> tcIfaceCoVar n
 tcIfaceCo (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n
                                                   <*> pure i
                                                   <*> mapM tcIfaceCo cs
-tcIfaceCo (IfaceUnivCo r t1 t2)     = UnivCo r <$> tcIfaceType t1
+tcIfaceCo (IfaceUnivCo s r t1 t2)   = UnivCo s r <$> tcIfaceType t1
                                                <*> tcIfaceType t2
 tcIfaceCo (IfaceSymCo c)            = SymCo    <$> tcIfaceCo c
 tcIfaceCo (IfaceTransCo c1 c2)      = TransCo  <$> tcIfaceCo c1
index 16d4bfc..ee97ee8 100644 (file)
@@ -1427,8 +1427,8 @@ zonkCoToCo env co
     go (TyConAppCo r tc args)    = mkTyConAppCo r tc <$> mapM go args
     go (AppCo co arg)            = mkAppCo <$> go co <*> go arg
     go (AxiomInstCo ax ind args) = AxiomInstCo ax ind <$> mapM go args
-    go (UnivCo r ty1 ty2)        = mkUnivCo r <$> zonkTcTypeToType env ty1
-                                              <*> zonkTcTypeToType env ty2
+    go (UnivCo s r ty1 ty2)      = mkUnivCo s r <$> zonkTcTypeToType env ty1
+                                                <*> zonkTcTypeToType env ty2
     go (SymCo co)                = mkSymCo <$> go co
     go (TransCo co1 co2)         = mkTransCo <$> go co1 <*> go co2
     go (NthCo n co)              = mkNthCo n <$> go co
index 7859203..e760cc4 100644 (file)
@@ -1496,7 +1496,7 @@ orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSet` orphNames
 orphNamesOfCo (ForAllCo _ co)       = orphNamesOfCo co
 orphNamesOfCo (CoVarCo _)           = emptyNameSet
 orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (UnivCo _ ty1 ty2)    = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
+orphNamesOfCo (UnivCo _ _ ty1 ty2)  = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
 orphNamesOfCo (SymCo co)            = orphNamesOfCo co
 orphNamesOfCo (TransCo co1 co2)     = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
 orphNamesOfCo (NthCo _ co)          = orphNamesOfCo co
index 71a003d..e55d526 100644 (file)
@@ -177,7 +177,8 @@ data Coercion
      -- See [Coercion axioms applied to coercions]
 
          -- see Note [UnivCo]
-  | UnivCo Role Type Type      -- :: "e" -> _ -> _ -> e
+  | UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e
+                               -- the FastString is just a note for provenance
   | SymCo Coercion             -- :: e -> e
   | TransCo Coercion Coercion  -- :: e -> e -> e
 
@@ -524,7 +525,7 @@ tyCoVarsOfCo (AppCo co1 co2)       = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo
 tyCoVarsOfCo (ForAllCo tv co)      = tyCoVarsOfCo co `delVarSet` tv
 tyCoVarsOfCo (CoVarCo v)           = unitVarSet v
 tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
-tyCoVarsOfCo (UnivCo _ ty1 ty2)    = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+tyCoVarsOfCo (UnivCo _ _ ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 tyCoVarsOfCo (SymCo co)            = tyCoVarsOfCo co
 tyCoVarsOfCo (TransCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
 tyCoVarsOfCo (NthCo _ co)          = tyCoVarsOfCo co
@@ -544,7 +545,7 @@ coVarsOfCo (AppCo co1 co2)       = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 coVarsOfCo (ForAllCo _ co)       = coVarsOfCo co
 coVarsOfCo (CoVarCo v)           = unitVarSet v
 coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
-coVarsOfCo (UnivCo _ _ _)        = emptyVarSet
+coVarsOfCo (UnivCo _ _ _ _)      = emptyVarSet
 coVarsOfCo (SymCo co)            = coVarsOfCo co
 coVarsOfCo (TransCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 coVarsOfCo (NthCo _ co)          = coVarsOfCo co
@@ -563,7 +564,7 @@ coercionSize (AppCo co1 co2)       = coercionSize co1 + coercionSize co2
 coercionSize (ForAllCo _ co)       = 1 + coercionSize co
 coercionSize (CoVarCo _)           = 1
 coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
-coercionSize (UnivCo _ ty1 ty2)  = typeSize ty1 + typeSize ty2
+coercionSize (UnivCo _ ty1 ty2)  = typeSize ty1 + typeSize ty2
 coercionSize (SymCo co)            = 1 + coercionSize co
 coercionSize (TransCo co1 co2)     = 1 + coercionSize co1 + coercionSize co2
 coercionSize (NthCo _ co)          = 1 + coercionSize co
@@ -597,7 +598,7 @@ tidyCo env@(_, subst) co
                                   Just cv' -> CoVarCo cv'
     go (AxiomInstCo con ind cos) = let args = tidyCos env cos
                                    in args `seqList` AxiomInstCo con ind args
-    go (UnivCo r ty1 ty2)     = (UnivCo r $! tidyType env ty1) $! tidyType env ty2
+    go (UnivCo s r ty1 ty2)   = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
     go (SymCo co)             = SymCo $! go co
     go (TransCo co1 co2)      = (TransCo $! go co1) $! go co2
     go (NthCo d co)           = NthCo d $! go co
@@ -658,7 +659,7 @@ ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                           pprParendCo co <> ptext (sLit "@") <> pprType ty
 
-ppr_co p (UnivCo r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ppr r)
+ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
                                            [pprParendType ty1, pprParendType ty2]
 ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
@@ -1008,7 +1009,7 @@ mkSymCo :: Coercion -> Coercion
 -- Do a few simple optimizations, but don't bother pushing occurrences
 -- of symmetry to the leaves; the optimizer will take care of that.
 mkSymCo co@(Refl {})             = co
-mkSymCo    (UnivCo r ty1 ty2)    = UnivCo r ty2 ty1
+mkSymCo    (UnivCo s r ty1 ty2)  = UnivCo s r ty2 ty1
 mkSymCo    (SymCo co)            = co
 mkSymCo co                       = SymCo co
 
@@ -1056,12 +1057,12 @@ mkInstCo co ty = InstCo co ty
 --   @unsafeCoerce#@ primitive.  Optimise by pushing
 --   down through type constructors.
 mkUnsafeCo :: Type -> Type -> Coercion
-mkUnsafeCo = mkUnivCo Representational
+mkUnsafeCo = mkUnivCo (fsLit "mkUnsafeCo") Representational
 
-mkUnivCo :: Role -> Type -> Type -> Coercion
-mkUnivCo role ty1 ty2
+mkUnivCo :: FastString -> Role -> Type -> Type -> Coercion
+mkUnivCo prov role ty1 ty2
   | ty1 `eqType` ty2 = Refl role ty1
-  | otherwise        = UnivCo role ty1 ty2
+  | otherwise        = UnivCo prov role ty1 ty2
 
 mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
 mkAxiomRuleCo = AxiomRuleCo
@@ -1071,7 +1072,7 @@ mkSubCo :: Coercion -> Coercion
 mkSubCo (Refl Nominal ty) = Refl Representational ty
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
-mkSubCo (UnivCo Nominal ty1 ty2) = UnivCo Representational ty1 ty2
+mkSubCo (UnivCo s Nominal ty1 ty2) = UnivCo s Representational ty1 ty2
 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
              SubCo co
 
@@ -1106,7 +1107,7 @@ setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
 setNominalRole_maybe (TyConAppCo Representational tc coes)
   = do { cos' <- mapM setNominalRole_maybe coes
        ; return $ TyConAppCo Nominal tc cos' }
-setNominalRole_maybe (UnivCo Representational ty1 ty2) = Just $ UnivCo Nominal ty1 ty2
+setNominalRole_maybe (UnivCo s Representational ty1 ty2) = Just $ UnivCo s Nominal ty1 ty2
   -- We do *not* promote UnivCo Phantom, as that's unsafe.
   -- UnivCo Nominal is no more unsafe than UnivCo Representational
 setNominalRole_maybe (TransCo co1 co2)
@@ -1125,7 +1126,7 @@ setNominalRole_maybe _ = Nothing
 mkPhantomCo :: Coercion -> Coercion
 mkPhantomCo co
   | Just ty <- isReflCo_maybe co    = Refl Phantom ty
-  | Pair ty1 ty2 <- coercionKind co = UnivCo Phantom ty1 ty2
+  | Pair ty1 ty2 <- coercionKind co = UnivCo (fsLit "mkPhantomCo") Phantom ty1 ty2
   -- don't optimise here... wait for OptCoercion
 
 -- All input coercions are assumed to be Nominal,
@@ -1355,7 +1356,8 @@ coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
     && ind1 == ind2
     && all2 (coreEqCoercion2 env) cos1 cos2
 
-coreEqCoercion2 env (UnivCo r1 ty11 ty12) (UnivCo r2 ty21 ty22)
+-- the provenance string is just a note, so don't use in comparisons
+coreEqCoercion2 env (UnivCo _ r1 ty11 ty12) (UnivCo _ r2 ty21 ty22)
   = r1 == r2 && eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
 
 coreEqCoercion2 env (SymCo co1) (SymCo co2)
@@ -1517,7 +1519,7 @@ subst_co subst co
                                    ForAllCo tv' $! subst_co subst' co
     go (CoVarCo cv)          = substCoVar subst cv
     go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
-    go (UnivCo r ty1 ty2)    = (UnivCo r $! go_ty ty1) $! go_ty ty2
+    go (UnivCo s r ty1 ty2)  = (UnivCo s r $! go_ty ty1) $! go_ty ty2
     go (SymCo co)            = mkSymCo (go co)
     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
     go (NthCo d co)          = mkNthCo d (go co)
@@ -1646,7 +1648,8 @@ ty_co_subst subst role ty
     go role ty@(LitTy {})     = ASSERT( role == Nominal )
                                 mkReflCo role ty
 
-    lift_phantom ty = mkUnivCo Phantom (liftCoSubstLeft  subst ty)
+    lift_phantom ty = mkUnivCo (fsLit "lift_phantom")
+                               Phantom (liftCoSubstLeft  subst ty)
                                        (liftCoSubstRight subst ty)
 
 {-
@@ -1817,7 +1820,7 @@ seqCo (AppCo co1 co2)           = seqCo co1 `seq` seqCo co2
 seqCo (ForAllCo tv co)          = tv `seq` seqCo co
 seqCo (CoVarCo cv)              = cv `seq` ()
 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
-seqCo (UnivCo r ty1 ty2)        = r `seq` seqType ty1 `seq` seqType ty2
+seqCo (UnivCo s r ty1 ty2)      = s `seq` r `seq` seqType ty1 `seq` seqType ty2
 seqCo (SymCo co)                = seqCo co
 seqCo (TransCo co1 co2)         = seqCo co1 `seq` seqCo co2
 seqCo (NthCo _ co)              = seqCo co
@@ -1877,7 +1880,7 @@ coercionKind co = go co
                                          -- exactly saturate the axiom branch
         Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
              (substTyWith tvs tys2 rhs)
-    go (UnivCo _ ty1 ty2)    = Pair ty1 ty2
+    go (UnivCo _ _ ty1 ty2)  = Pair ty1 ty2
     go (SymCo co)            = swap $ go co
     go (TransCo co1 co2)     = Pair (pFst $ go co1) (pSnd $ go co2)
     go (NthCo d co)          = tyConAppArgN d <$> go co
@@ -1915,7 +1918,7 @@ coercionKindRole = go
         (mkForAllTy tv <$> tys, r)
     go (CoVarCo cv) = (toPair $ coVarKind cv, coVarRole cv)
     go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
-    go (UnivCo r ty1 ty2) = (Pair ty1 ty2, r)
+    go (UnivCo r ty1 ty2) = (Pair ty1 ty2, r)
     go (SymCo co) = first swap $ go co
     go (TransCo co1 co2)
       = let (tys1, r) = go co1 in
index b75cd30..c889f8a 100644 (file)
@@ -199,9 +199,9 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos)
                                  cos)
       -- Note that the_co does *not* have sym pushed into it
 
-opt_co4 env sym rep r (UnivCo _r oty1 oty2)
+opt_co4 env sym rep r (UnivCo _r oty1 oty2)
   = ASSERT( r == _r )
-    opt_univ env (chooseRole rep r) a b
+    opt_univ env (chooseRole rep r) a b
   where
     (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
 
@@ -266,24 +266,24 @@ opt_co4 env sym rep r (AxiomRuleCo co ts cs)
 opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
 opt_phantom env sym co
   = if sym
-    then opt_univ env Phantom ty2 ty1
-    else opt_univ env Phantom ty1 ty2
+    then opt_univ env (fsLit "opt_phantom") Phantom ty2 ty1
+    else opt_univ env (fsLit "opt_phantom") Phantom ty1 ty2
   where
     Pair ty1 ty2 = coercionKind co
 
-opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
-opt_univ env role oty1 oty2
+opt_univ :: CvSubst -> FastString -> Role -> Type -> Type -> Coercion
+opt_univ env prov role oty1 oty2
   | Just (tc1, tys1) <- splitTyConApp_maybe oty1
   , Just (tc2, tys2) <- splitTyConApp_maybe oty2
   , tc1 == tc2
-  = mkTyConAppCo role tc1 (zipWith3 (opt_univ env) (tyConRolesX role tc1) tys1 tys2)
+  = mkTyConAppCo role tc1 (zipWith3 (opt_univ env prov) (tyConRolesX role tc1) tys1 tys2)
 
   | Just (l1, r1) <- splitAppTy_maybe oty1
   , Just (l2, r2) <- splitAppTy_maybe oty2
   , typeKind l1 `eqType` typeKind l2   -- kind(r1) == kind(r2) by consequence
   = let role' = if role == Phantom then Phantom else Nominal in
        -- role' is to comform to mkAppCo's precondition
-    mkAppCo (opt_univ env role l1 l2) (opt_univ env role' r1 r2)
+    mkAppCo (opt_univ env prov role l1 l2) (opt_univ env prov role' r1 r2)
 
   | Just (tv1, ty1) <- splitForAllTy_maybe oty1
   , Just (tv2, ty2) <- splitForAllTy_maybe oty2
@@ -291,10 +291,10 @@ opt_univ env role oty1 oty2
   = case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
     let ty1' = substTy env1 ty1
         ty2' = substTy env2 ty2 in
-    mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) role ty1' ty2') }
+    mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) prov role ty1' ty2') }
 
   | otherwise
-  = mkUnivCo role (substTy env oty1) (substTy env oty2)
+  = mkUnivCo prov role (substTy env oty1) (substTy env oty2)
 
 -------------
 -- NthCo must be handled separately, because it's the one case where we can't