[commit: ghc] wip/rae-new-coercible: Zonk Coercions embedded in TcCoercions; they *might* have TcTyVars! (1900380)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/rae-new-coercible
Link       : http://ghc.haskell.org/trac/ghc/changeset/190038033778925092b03169d33e29f4c8e5fb05/ghc

>---------------------------------------------------------------

commit 190038033778925092b03169d33e29f4c8e5fb05
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Fri Dec 12 12:01:58 2014 -0500

    Zonk Coercions embedded in TcCoercions; they *might* have TcTyVars!


>---------------------------------------------------------------

190038033778925092b03169d33e29f4c8e5fb05
 compiler/typecheck/TcHsSyn.hs | 31 ++++++++++++++++++++++++++++---
 1 file changed, 28 insertions(+), 3 deletions(-)

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 4b7b930..a0433f9 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1411,7 +1411,7 @@ zonkTcTypeToType env ty
         -- The two interesting cases!
     go (TyVarTy tv) = zonkTyVarOcc env tv
 
-    go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) do
+    go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv )
                           do { (env', tv') <- zonkTyBndrX env tv
                              ; ty' <- zonkTcTypeToType env' ty
                              ; return (ForAllTy tv' ty') }
@@ -1419,6 +1419,32 @@ zonkTcTypeToType env ty
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 
+zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
+zonkCoToCo env co
+  = go co
+  where
+    go (Refl r ty)               = mkReflCo r <$> zonkTcTypeToType env ty
+    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) = mkAxiomInstCo ax ind <$> mapM go args
+    go (UnivCo r ty1 ty2)        = mkUnivCo 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
+    go (LRCo lr co)              = mkLRCo lr <$> go co
+    go (InstCo co arg)           = mkInstCo <$> go co <*> zonkCoArgToCoArg env arg
+    go (SubCo co)                = mkSubCo <$> go co
+    go (AxiomRuleCo ax ts cs)    = AxiomRuleCo ax <$> mapM (zonkTcTypeToType env) ts
+                                                  <*> mapM go cs
+
+    -- The two interesting cases!
+    go (CoVarCo cv)              = return (mkCoVarCo $ zonkIdOcc env cv)
+    go (ForAllCo tv co)          = ASSERT( isImmutableTyVar tv )
+                                   do { (env', tv') <- zonkTyBndrX env tv
+                                      ; co' <- zonkCoToCo env' co
+                                      ; return (mkForAllCo tv' co') }
+                                   
 zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker
 -- This variant collects unbound type variables in a mutable variable
 -- Works on both types and kinds
@@ -1481,5 +1507,4 @@ zonkTcCoToCo env co
                                      ; cs' <- mapM go cs
                                      ; return (TcAxiomRuleCo co ts' cs')
                                      }
-    go c@(TcCoercion _co)     = ASSERT( isEmptyVarSet (coVarsOfCo _co) )
-                                return c   -- these can't contain TcTyVars
+    go (TcCoercion co)        = do { co' <- zonkCoToCo co; return (TcCoercion co') }