Treat isConstraintKind more consistently
[ghc.git] / compiler / types / Unify.hs
index 94ee3f8..5248b72 100644 (file)
@@ -31,7 +31,6 @@ import GhcPrelude
 import Var
 import VarEnv
 import VarSet
-import Kind
 import Name( Name )
 import Type hiding ( getTvSubstEnv )
 import Coercion hiding ( getCvSubstEnv )
@@ -85,7 +84,7 @@ How do you choose between them?
 1. If you know that the kinds of the two types are eqType, use
    the Ty variant. It is more efficient, as it does less work.
 
-2. If the kinds of variables in the  template type might mention type families,
+2. If the kinds of variables in the template type might mention type families,
    use the Ty variant (and do other work to make sure the kinds
    work out). These pure unification functions do a straightforward
    syntactic unification and do no complex reasoning about type
@@ -96,9 +95,9 @@ How do you choose between them?
    families in kinds in the TyKi variant. You just might get match
    failure even though a reducing a type family would lead to success.)
 
-3. Otherwise, if you're sure that the variable kinds to not mention
+3. Otherwise, if you're sure that the variable kinds do not mention
    type families and you're not already sure that the kind of the template
-   equals the kind of the target, then use the TyKi versio.n
+   equals the kind of the target, then use the TyKi version.
 -}
 
 -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
@@ -502,7 +501,7 @@ tc_unify_tys :: (TyVar -> BindFlag)
 -- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
 -- the kinds of the types should be the same. However, this doesn't work,
 -- as the types may be a dependent telescope, where later types have kinds
--- that mention variables occuring earlier in the list of types. Here's an
+-- that mention variables occurring earlier in the list of types. Here's an
 -- example (from typecheck/should_fail/T12709):
 --   template: [rep :: RuntimeRep,       a :: TYPE rep]
 --   target:   [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
@@ -598,10 +597,10 @@ So, we work as follows:
     tyvars, extending it each time with a new binding, so we
     finish up with
        [ xs   :-> ..as before..
-       , a    :-> ..as before..
+       , a    :-> b
        , b    :-> b    :: *
        , z    :-> z    :: b
-       , rest :-> rest :: G a (z :: b) ]
+       , rest :-> rest :: G b (z :: b) ]
     Note that rest now has the right kind
 
  7. Apply this extended substitution (once) to the range of
@@ -1319,7 +1318,7 @@ data MatchEnv = ME { me_tmpls :: TyVarSet
                    , me_env   :: RnEnv2 }
 
 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
---   @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
+--   @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@,
 --   where @==@ there means that the result of 'liftCoSubst' has the same
 --   type as the original co; but may be different under the hood.
 --   That is, it matches a type against a coercion of the same
@@ -1392,9 +1391,6 @@ ty_co_match menv subst ty co lkco rkco
     ty_co_match menv subst ty' co (substed_co_l `mkTransCo` lkco)
                                   (substed_co_r `mkTransCo` rkco)
 
-  | CoherenceCo co1 co2 <- co
-  = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
-
   | SymCo co' <- co
   = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
 
@@ -1409,7 +1405,7 @@ ty_co_match menv subst (TyVarTy tv1) co lkco rkco
   = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
     then Nothing      -- occurs check failed
     else Just $ extendVarEnv subst tv1' $
-                castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
+                castCoercionKindI co (mkSymCo lkco) (mkSymCo rkco)
 
   | otherwise
   = Nothing
@@ -1457,6 +1453,21 @@ ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
 ty_co_match _ subst (CoercionTy {}) _ _ _
   = Just subst -- don't inspect coercions
 
+ty_co_match menv subst ty (GRefl r t (MCo co)) lkco rkco
+  =  ty_co_match menv subst ty (GRefl r t MRefl) lkco (rkco `mkTransCo` mkSymCo co)
+
+ty_co_match menv subst ty co1 lkco rkco
+  | Just (CastTy t co, r) <- isReflCo_maybe co1
+  -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us
+  -- t |> co ~ t ; <t> ; t ~ t |> co
+  -- But transitive coercions are not helpful. Therefore we deal
+  -- with it here: we do recursion on the smaller reflexive coercion,
+  -- while propagating the correct kind coercions.
+  = let kco' = mkSymCo co
+    in ty_co_match menv subst ty (mkReflCo r t) (lkco `mkTransCo` kco')
+                                                (rkco `mkTransCo` kco')
+
+
 ty_co_match menv subst ty co lkco rkco
   | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
   | otherwise               = Nothing
@@ -1501,17 +1512,18 @@ ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
 ty_co_match_args _    _     _        _          _ _ = Nothing
 
 pushRefl :: Coercion -> Maybe Coercion
-pushRefl (Refl Nominal (AppTy ty1 ty2))
-  = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
-pushRefl (Refl r (FunTy ty1 ty2))
-  | Just rep1 <- getRuntimeRep_maybe ty1
-  , Just rep2 <- getRuntimeRep_maybe ty2
-  = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
-                                , mkReflCo r ty1,  mkReflCo r ty2 ])
-pushRefl (Refl r (TyConApp tc tys))
-  = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
-pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
-  = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
+pushRefl co =
+  case (isReflCo_maybe co) of
+    Just (AppTy ty1 ty2, Nominal)
+      -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2))
+    Just (FunTy ty1 ty2, r)
+      | Just rep1 <- getRuntimeRep_maybe ty1
+      , Just rep2 <- getRuntimeRep_maybe ty2
+      ->  Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
+                                       , mkReflCo r ty1,  mkReflCo r ty2 ])
+    Just (TyConApp tc tys, r)
+      -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
+    Just (ForAllTy (TvBndr tv _) ty, r)
+      -> Just (mkHomoForAllCos_NoRefl [tv] (mkReflCo r ty))
     -- NB: NoRefl variant. Otherwise, we get a loop!
-pushRefl (Refl r (CastTy ty co))  = Just (castCoercionKind (Refl r ty) co co)
-pushRefl _                        = Nothing
+    _ -> Nothing