Fix corner case in typeKind, plus refactoring
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 15 Jun 2018 08:19:55 +0000 (09:19 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 15 Jun 2018 08:47:06 +0000 (09:47 +0100)
This is a continuation of

    commit 9d600ea68c283b0d38ac663c3cc48baba6b94f57
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Fri Jun 1 16:36:57 2018 +0100

        Expand type synonyms when Linting a forall

That patch pointed out that there was a lurking hole in
typeKind, where it could return an ill-scoped kind, because
of not expanding type synonyms enough.

This patch fixes it, quite nicely

* Use occCheckExpand to expand those synonyms (it was always
  designed for that exact purpose), and call it from
         Type.typeKind
         CoreUtils.coreAltType
         CoreLint.lintTYpe

* Consequently, move occCheckExpand from TcUnify.hs to
  Type.hs, and generalise it to take a list of type variables.

I also tidied up lintType a bit.

compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CoreUtils.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcUnify.hs
compiler/types/Coercion.hs-boot
compiler/types/Type.hs

index 517b1be..90095ad 100644 (file)
@@ -715,8 +715,7 @@ lintCoreExpr (Cast expr co)
   = do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
        ; co' <- applySubstCo co
        ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
-       ; lintL (classifiesTypeWithValues k2)
-               (text "Target of cast not # or *:" <+> ppr co)
+       ; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
        ; lintRole co' Representational r
        ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
        ; return to_ty }
@@ -1296,8 +1295,9 @@ lintInTy ty
   = addLoc (InType ty) $
     do  { ty' <- applySubstTy ty
         ; k  <- lintType ty'
-        -- No need to lint k, because lintType
-        -- guarantees that k is linted
+        ; lintKind k  -- The kind returned by lintType is already
+                      -- a LintedKind but we also want to check that
+                      -- k :: *, which lintKind does
         ; return (ty', k) }
 
 checkTyCon :: TyCon -> LintM ()
@@ -1357,18 +1357,13 @@ lintType t@(ForAllTy (TvBndr tv _vis) ty)
   = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
        ; lintTyBndr tv $ \tv' ->
     do { k <- lintType ty
-       ; lintL (classifiesTypeWithValues k)
-               (text "Non-* and non-# kind in forall:" <+> ppr t)
-       ; if (not (tv' `elemVarSet` tyCoVarsOfType k))
-         then return k
-         else
-    do { -- See Note [Stupid type synonyms]
-         let k' = expandTypeSynonyms k
-       ; lintL (not (tv' `elemVarSet` tyCoVarsOfType k'))
-               (hang (text "Variable escape in forall:")
-                   2 (vcat [ text "type:" <+> ppr t
-                           , text "kind:" <+> ppr k' ]))
-       ; return k' }}}
+       ; checkValueKind k (text "the body of forall:" <+> ppr t)
+       ; case occCheckExpand [tv'] k of  -- See Note [Stupid type synonyms]
+           Just k' -> return k'
+           Nothing -> failWithL (hang (text "Variable escape in forall:")
+                                    2 (vcat [ text "type:" <+> ppr t
+                                            , text "kind:" <+> ppr k ]))
+    }}
 
 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
 
@@ -1429,9 +1424,9 @@ lintKind k = do { sk <- lintType k
                                       2 (text "has kind:" <+> ppr sk))) }
 
 -----------------
--- confirms that a type is really *
-lintStar :: SDoc -> OutKind -> LintM ()
-lintStar doc k
+-- Confirms that a type is really *, #, Constraint etc
+checkValueKind :: OutKind -> SDoc -> LintM ()
+checkValueKind k doc
   = lintL (classifiesTypeWithValues k)
           (text "Non-*-like kind when *-like expected:" <+> ppr k $$
            text "when checking" <+> doc)
@@ -1618,8 +1613,8 @@ lintInCo co
 lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
 lintStarCoercion g
   = do { (k1, k2, t1, t2, r) <- lintCoercion g
-       ; lintStar (text "the kind of the left type in" <+> ppr g) k1
-       ; lintStar (text "the kind of the right type in" <+> ppr g) k2
+       ; checkValueKind k1 (text "the kind of the left type in" <+> ppr g)
+       ; checkValueKind k2 (text "the kind of the right type in" <+> ppr g)
        ; lintRole g Nominal r
        ; return (t1, t2) }
 
index 7fc9fb3..88e1f71 100644 (file)
@@ -130,13 +130,13 @@ exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy
 
 coreAltType :: CoreAlt -> Type
 -- ^ Returns the type of the alternatives right hand side
-coreAltType (_,bs,rhs)
-  | any bad_binder bs = expandTypeSynonyms ty
-  | otherwise         = ty    -- Note [Existential variables and silly type synonyms]
+coreAltType alt@(_,bs,rhs)
+  = case occCheckExpand bs rhs_ty of
+      -- Note [Existential variables and silly type synonyms]
+      Just ty -> ty
+      Nothing -> pprPanic "coreAltType" (pprCoreAlt alt $$ ppr rhs_ty)
   where
-    ty           = exprType rhs
-    free_tvs     = tyCoVarsOfType ty
-    bad_binder b = b `elemVarSet` free_tvs
+    rhs_ty = exprType rhs
 
 coreAltsType :: [CoreAlt] -> Type
 -- ^ Returns the type of the first alternative, which should be the same as for all alternatives
index 32a9307..f4176f5 100644 (file)
@@ -14,7 +14,6 @@ import GhcPrelude
 import TcRnTypes
 import TcType
 import Type
-import TcUnify( occCheckExpand )
 import TcEvidence
 import TyCon
 import TyCoRep   -- performs delicate algorithm on types
@@ -1994,7 +1993,7 @@ unflattenWanteds tv_eqs funeqs
                -- to observe the occurs check.  Zonking will eliminate it
                -- altogether in due course
              rhs' <- zonkTcType (mkTyConApp tc xis)
-           ; case occCheckExpand fmv rhs' of
+           ; case occCheckExpand [fmv] rhs' of
                Just rhs''    -- Normal case: fill the tyvar
                  -> do { setReflEvidence ev NomEq rhs''
                        ; unflattenFmv fmv rhs''
@@ -2092,7 +2091,7 @@ tryFill ev tv rhs
               , tv == tv'   -- tv == rhs
               -> return True
 
-            _ | Just rhs'' <- occCheckExpand tv rhs'
+            _ | Just rhs'' <- occCheckExpand [tv] rhs'
               -> do {       -- Fill the tyvar
                       unifyTyVar tv rhs''
                     ; return True }
index be0586e..fa845bb 100644 (file)
@@ -31,8 +31,7 @@ module TcUnify (
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  occCheckExpand, metaTyVarUpdateOK,
-  occCheckForErrors, OccCheckResult(..)
+  metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
 
   ) where
 
@@ -61,7 +60,6 @@ import DynFlags
 import BasicTypes
 import Bag
 import Util
-import Pair( pFst )
 import qualified GHC.LanguageExtensions as LangExt
 import Outputable
 
@@ -1985,34 +1983,8 @@ matchExpectedFunKind hs_ty = go
 ********************************************************************* -}
 
 
-{- Note [Occurs check expansion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
-of occurrences of tv outside type function arguments, if that is
-possible; otherwise, it returns Nothing.
-
-For example, suppose we have
-  type F a b = [a]
-Then
-  occCheckExpand b (F Int b) = Just [Int]
-but
-  occCheckExpand a (F a Int) = Nothing
-
-We don't promise to do the absolute minimum amount of expanding
-necessary, but we try not to do expansions we don't need to.  We
-prefer doing inner expansions first.  For example,
-  type F a b = (a, Int, a, [a])
-  type G b   = Char
-We have
-  occCheckExpand b (F (G b)) = Just (F Char)
-even though we could also expand F to get rid of b.
-
-The two variants of the function are to support TcUnify.checkTauTvUpdate,
-which wants to prevent unification with type families. For more on this
-point, see Note [Prevent unification with type families] in TcUnify.
-
-Note [Occurrence checking: look inside kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{-  Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are considering unifying
    (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
 This may be an error (what is that alpha doing inside beta's kind?),
@@ -2083,7 +2055,7 @@ occCheckForErrors dflags tv ty
   = case preCheck dflags True tv ty of
       OC_OK _   -> OC_OK ()
       OC_Bad    -> OC_Bad
-      OC_Occurs -> case occCheckExpand tv ty of
+      OC_Occurs -> case occCheckExpand [tv] ty of
                      Nothing -> OC_Occurs
                      Just _  -> OC_OK ()
 
@@ -2121,7 +2093,7 @@ metaTyVarUpdateOK dflags tv ty
          -- See Note [Prevent unification with type families]
       OC_OK _   -> Just ty
       OC_Bad    -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand tv ty
+      OC_Occurs -> occCheckExpand [tv] ty
 
 preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
 -- A quick check for
@@ -2182,121 +2154,6 @@ preCheck dflags ty_fam_ok tv ty
       | not (ty_fam_ok        || isFamFreeTyCon tc) = True
       | otherwise                                   = False
 
-occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
--- See Note [Occurs check expansion]
--- We may have needed to do some type synonym unfolding in order to
--- get rid of the variable (or forall), so we also return the unfolded
--- version of the type, which is guaranteed to be syntactically free
--- of the given type variable.  If the type is already syntactically
--- free of the variable, then the same type is returned.
-occCheckExpand tv ty
-  = go emptyVarEnv ty
-  where
-    go :: VarEnv TyVar -> Type -> Maybe Type
-          -- The VarEnv carries mappings necessary
-          -- because of kind expansion
-    go env (TyVarTy tv')
-      | tv == tv'                         = Nothing
-      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
-      | otherwise                         = do { tv'' <- go_var env tv'
-                                               ; return (mkTyVarTy tv'') }
-
-    go _   ty@(LitTy {}) = return ty
-    go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
-                                ; ty2' <- go env ty2
-                                ; return (mkAppTy ty1' ty2') }
-    go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
-                                ; ty2' <- go env ty2
-                                ; return (mkFunTy ty1' ty2') }
-    go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
-       | tv == tv'         = return ty
-       | otherwise         = do { ki' <- go env (tyVarKind tv')
-                                ; let tv'' = setTyVarKind tv' ki'
-                                      env' = extendVarEnv env tv' tv''
-                                ; body' <- go env' body_ty
-                                ; return (ForAllTy (TvBndr tv'' vis) body') }
-
-    -- For a type constructor application, first try expanding away the
-    -- offending variable from the arguments.  If that doesn't work, next
-    -- see if the type constructor is a type synonym, and if so, expand
-    -- it and try again.
-    go env ty@(TyConApp tc tys)
-      = case mapM (go env) tys of
-          Just tys' -> return (mkTyConApp tc tys')
-          Nothing | Just ty' <- tcView ty -> go env ty'
-                  | otherwise             -> Nothing
-                      -- Failing that, try to expand a synonym
-
-    go env (CastTy ty co) =  do { ty' <- go env ty
-                                ; co' <- go_co env co
-                                ; return (mkCastTy ty' co') }
-    go env (CoercionTy co) = do { co' <- go_co env co
-                                ; return (mkCoercionTy co') }
-
-    ------------------
-    go_var env v = do { k' <- go env (varType v)
-                      ; return (setVarType v k') }
-           -- Works for TyVar and CoVar
-           -- See Note [Occurrence checking: look inside kinds]
-
-    ------------------
-    go_co env (Refl r ty)               = do { ty' <- go env ty
-                                             ; return (mkReflCo r ty') }
-      -- Note: Coercions do not contain type synonyms
-    go_co env (TyConAppCo r tc args)    = do { args' <- mapM (go_co env) args
-                                             ; return (mkTyConAppCo r tc args') }
-    go_co env (AppCo co arg)            = do { co' <- go_co env co
-                                             ; arg' <- go_co env arg
-                                             ; return (mkAppCo co' arg') }
-    go_co env co@(ForAllCo tv' kind_co body_co)
-      | tv == tv'         = return co
-      | otherwise         = do { kind_co' <- go_co env kind_co
-                               ; let tv'' = setTyVarKind tv' $
-                                            pFst (coercionKind kind_co')
-                                     env' = extendVarEnv env tv' tv''
-                               ; body' <- go_co env' body_co
-                               ; return (ForAllCo tv'' kind_co' body') }
-    go_co env (FunCo r co1 co2)         = do { co1' <- go_co env co1
-                                             ; co2' <- go_co env co2
-                                             ; return (mkFunCo r co1' co2') }
-    go_co env (CoVarCo c)               = do { c' <- go_var env c
-                                             ; return (mkCoVarCo c') }
-    go_co env (HoleCo h)                = do { c' <- go_var env (ch_co_var h)
-                                             ; return (HoleCo (h { ch_co_var = c' })) }
-    go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
-                                             ; return (mkAxiomInstCo ax ind args') }
-    go_co env (UnivCo p r ty1 ty2)      = do { p' <- go_prov env p
-                                             ; ty1' <- go env ty1
-                                             ; ty2' <- go env ty2
-                                             ; return (mkUnivCo p' r ty1' ty2') }
-    go_co env (SymCo co)                = do { co' <- go_co env co
-                                             ; return (mkSymCo co') }
-    go_co env (TransCo co1 co2)         = do { co1' <- go_co env co1
-                                             ; co2' <- go_co env co2
-                                             ; return (mkTransCo co1' co2') }
-    go_co env (NthCo r n co)            = do { co' <- go_co env co
-                                             ; return (mkNthCo r n co') }
-    go_co env (LRCo lr co)              = do { co' <- go_co env co
-                                             ; return (mkLRCo lr co') }
-    go_co env (InstCo co arg)           = do { co' <- go_co env co
-                                             ; arg' <- go_co env arg
-                                             ; return (mkInstCo co' arg') }
-    go_co env (CoherenceCo co1 co2)     = do { co1' <- go_co env co1
-                                             ; co2' <- go_co env co2
-                                             ; return (mkCoherenceCo co1' co2') }
-    go_co env (KindCo co)               = do { co' <- go_co env co
-                                             ; return (mkKindCo co') }
-    go_co env (SubCo co)                = do { co' <- go_co env co
-                                             ; return (mkSubCo co') }
-    go_co env (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co env) cs
-                                             ; return (mkAxiomRuleCo ax cs') }
-
-    ------------------
-    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
-    go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
-    go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
-    go_prov _   p@(PluginProv _)    = return p
-
 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
 canUnifyWithPolyType dflags details
   = case details of
index 15e4585..df4a24e 100644 (file)
@@ -32,6 +32,7 @@ mkCoherenceCo :: Coercion -> Coercion -> Coercion
 mkKindCo :: Coercion -> Coercion
 mkSubCo :: Coercion -> Coercion
 mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
+mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 
 isReflCo :: Coercion -> Bool
 isReflexiveCo :: Coercion -> Bool
index 963fad4..9c88c11 100644 (file)
@@ -133,7 +133,7 @@ module Type (
         noFreeVarsOfType,
         splitVisVarsOfType, splitVisVarsOfTypes,
         expandTypeSynonyms,
-        typeSize,
+        typeSize, occCheckExpand,
 
         -- * Well-scoped lists of variables
         dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
@@ -2320,16 +2320,20 @@ nonDetCmpTc tc1 tc2
 -}
 
 typeKind :: HasDebugCallStack => Type -> Kind
-typeKind (TyConApp tc tys)     = piResultTys (tyConKind tc) tys
-typeKind (AppTy fun arg)       = typeKind_apps fun [arg]
-typeKind (LitTy l)             = typeLiteralKind l
-typeKind (FunTy {})            = liftedTypeKind
-typeKind (TyVarTy tyvar)       = tyVarKind tyvar
-typeKind (CastTy _ty co)       = pSnd $ coercionKind co
-typeKind (CoercionTy co)       = coercionType co
-typeKind (ForAllTy _ ty)       = typeKind ty -- Urk. See Note [Stupid type synonyms]
-                                             -- in CoreLint.  Maybe we should do
-                                             -- something similar here...
+typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
+typeKind (AppTy fun arg)   = typeKind_apps fun [arg]
+typeKind (LitTy l)         = typeLiteralKind l
+typeKind (FunTy {})        = liftedTypeKind
+typeKind (TyVarTy tyvar)   = tyVarKind tyvar
+typeKind (CastTy _ty co)   = pSnd $ coercionKind co
+typeKind (CoercionTy co)   = coercionType co
+typeKind ty@(ForAllTy {})  = case occCheckExpand tvs k of
+                               Just k' -> k'
+                               Nothing -> pprPanic "typeKind"
+                                            (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
+                           where
+                             (tvs, body) = splitForAllTys ty
+                             k           = typeKind body
 
 typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
 -- The sole purpose of the function is to accumulate
@@ -2370,6 +2374,153 @@ isTypeLevPoly = go
 resultIsLevPoly :: Type -> Bool
 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
 
+
+{- **********************************************************************
+*                                                                       *
+           Occurs check expansion
+%*                                                                      *
+%********************************************************************* -}
+
+{- Note [Occurs check expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
+of occurrences of tv outside type function arguments, if that is
+possible; otherwise, it returns Nothing.
+
+For example, suppose we have
+  type F a b = [a]
+Then
+  occCheckExpand b (F Int b) = Just [Int]
+but
+  occCheckExpand a (F a Int) = Nothing
+
+We don't promise to do the absolute minimum amount of expanding
+necessary, but we try not to do expansions we don't need to.  We
+prefer doing inner expansions first.  For example,
+  type F a b = (a, Int, a, [a])
+  type G b   = Char
+We have
+  occCheckExpand b (F (G b)) = Just (F Char)
+even though we could also expand F to get rid of b.
+-}
+
+occCheckExpand :: [Var] -> Type -> Maybe Type
+-- See Note [Occurs check expansion]
+-- We may have needed to do some type synonym unfolding in order to
+-- get rid of the variable (or forall), so we also return the unfolded
+-- version of the type, which is guaranteed to be syntactically free
+-- of the given type variable.  If the type is already syntactically
+-- free of the variable, then the same type is returned.
+occCheckExpand vs_to_avoid ty
+  = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
+  where
+    go :: (VarSet, VarEnv TyVar) -> Type -> Maybe Type
+          -- The VarSet is the set of variables we are trying to avoid
+          -- The VarEnv carries mappings necessary
+          -- because of kind expansion
+    go cxt@(as, env) (TyVarTy tv')
+      | tv' `elemVarSet` as               = Nothing
+      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
+      | otherwise                         = do { tv'' <- go_var cxt tv'
+                                               ; return (mkTyVarTy tv'') }
+
+    go _   ty@(LitTy {}) = return ty
+    go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
+                                ; ty2' <- go cxt ty2
+                                ; return (mkAppTy ty1' ty2') }
+    go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
+                                ; ty2' <- go cxt ty2
+                                ; return (mkFunTy ty1' ty2') }
+    go cxt@(as, env) (ForAllTy (TvBndr tv vis) body_ty)
+       = do { ki' <- go cxt (tyVarKind tv)
+            ; let tv' = setTyVarKind tv ki'
+                  env' = extendVarEnv env tv tv'
+                  as'  = as `delVarSet` tv
+            ; body' <- go (as', env') body_ty
+            ; return (ForAllTy (TvBndr tv' vis) body') }
+
+    -- For a type constructor application, first try expanding away the
+    -- offending variable from the arguments.  If that doesn't work, next
+    -- see if the type constructor is a type synonym, and if so, expand
+    -- it and try again.
+    go cxt ty@(TyConApp tc tys)
+      = case mapM (go cxt) tys of
+          Just tys' -> return (mkTyConApp tc tys')
+          Nothing | Just ty' <- tcView ty -> go cxt ty'
+                  | otherwise             -> Nothing
+                      -- Failing that, try to expand a synonym
+
+    go cxt (CastTy ty co) =  do { ty' <- go cxt ty
+                                ; co' <- go_co cxt co
+                                ; return (mkCastTy ty' co') }
+    go cxt (CoercionTy co) = do { co' <- go_co cxt co
+                                   ; return (mkCoercionTy co') }
+
+    ------------------
+    go_var cxt v = do { k' <- go cxt (varType v)
+                      ; return (setVarType v k') }
+           -- Works for TyVar and CoVar
+           -- See Note [Occurrence checking: look inside kinds]
+
+    ------------------
+    go_co cxt (Refl r ty)               = do { ty' <- go cxt ty
+                                             ; return (mkReflCo r ty') }
+      -- Note: Coercions do not contain type synonyms
+    go_co cxt (TyConAppCo r tc args)    = do { args' <- mapM (go_co cxt) args
+                                             ; return (mkTyConAppCo r tc args') }
+    go_co cxt (AppCo co arg)            = do { co' <- go_co cxt co
+                                             ; arg' <- go_co cxt arg
+                                             ; return (mkAppCo co' arg') }
+    go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
+      = do { kind_co' <- go_co cxt kind_co
+           ; let tv' = setTyVarKind tv $
+                       pFst (coercionKind kind_co')
+                 env' = extendVarEnv env tv tv'
+                 as'  = as `delVarSet` tv
+           ; body' <- go_co (as', env') body_co
+           ; return (ForAllCo tv' kind_co' body') }
+    go_co cxt (FunCo r co1 co2)         = do { co1' <- go_co cxt co1
+                                             ; co2' <- go_co cxt co2
+                                             ; return (mkFunCo r co1' co2') }
+    go_co cxt (CoVarCo c)               = do { c' <- go_var cxt c
+                                             ; return (mkCoVarCo c') }
+    go_co cxt (HoleCo h)                = do { c' <- go_var cxt (ch_co_var h)
+                                             ; return (HoleCo (h { ch_co_var = c' })) }
+    go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
+                                             ; return (mkAxiomInstCo ax ind args') }
+    go_co cxt (UnivCo p r ty1 ty2)      = do { p' <- go_prov cxt p
+                                             ; ty1' <- go cxt ty1
+                                             ; ty2' <- go cxt ty2
+                                             ; return (mkUnivCo p' r ty1' ty2') }
+    go_co cxt (SymCo co)                = do { co' <- go_co cxt co
+                                             ; return (mkSymCo co') }
+    go_co cxt (TransCo co1 co2)         = do { co1' <- go_co cxt co1
+                                             ; co2' <- go_co cxt co2
+                                             ; return (mkTransCo co1' co2') }
+    go_co cxt (NthCo r n co)            = do { co' <- go_co cxt co
+                                             ; return (mkNthCo r n co') }
+    go_co cxt (LRCo lr co)              = do { co' <- go_co cxt co
+                                             ; return (mkLRCo lr co') }
+    go_co cxt (InstCo co arg)           = do { co' <- go_co cxt co
+                                             ; arg' <- go_co cxt arg
+                                             ; return (mkInstCo co' arg') }
+    go_co cxt (CoherenceCo co1 co2)     = do { co1' <- go_co cxt co1
+                                             ; co2' <- go_co cxt co2
+                                             ; return (mkCoherenceCo co1' co2') }
+    go_co cxt (KindCo co)               = do { co' <- go_co cxt co
+                                             ; return (mkKindCo co') }
+    go_co cxt (SubCo co)                = do { co' <- go_co cxt co
+                                             ; return (mkSubCo co') }
+    go_co cxt (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co cxt) cs
+                                             ; return (mkAxiomRuleCo ax cs') }
+
+    ------------------
+    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
+    go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
+    go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
+    go_prov _   p@(PluginProv _)    = return p
+
+
 {-
 %************************************************************************
 %*                                                                      *