Wibbleswip/T22194

3 files changed, 56 insertions, 37 deletions

diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 9b068e18e6..bdc15f4510 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -1843,6 +1843,9 @@ Wrinkles:
      and unifying alpha effectively promotes this wanted to a given. Doing so
      means we lose track of the rewriter set associated with the wanted.
 
+     In short: we must not have a co_hole in a Given, and unification
+     effectively makes a Given
+
      On the other hand, w is perfectly suitable for rewriting, because of the
      way we carefully track rewriter sets.
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 6fc04c7f08..c4bb1157db 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -2074,23 +2074,23 @@ checkTouchableTyVarEq
 --   with extra wanteds 'cts'
 -- If it returns (PuFail reason) we can't unify, and the reason explains why.
 checkTouchableTyVarEq ev lhs_tv rhs
-  | MetaTv { mtv_info = lhs_tv_info, mtv_tclvl = lhs_tv_lvl } <- tcTyVarDetails lhs_tv
   = do { traceTcS "checkTouchableTyVarEq" (ppr lhs_tv $$ ppr rhs)
-       ; check_result <- wrapTcS (check_rhs lhs_tv_info lhs_tv_lvl)
+       ; check_result <- wrapTcS check_rhs
        ; traceTcS "checkTouchableTyVarEq 2" (ppr lhs_tv $$ ppr check_result)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
             PuOK redn cts -> do { emitWork (bagToList cts)
                                 ; return (pure redn) } }
-
-  | otherwise = pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
   where
     ghci_tv = isRuntimeUnkSkol lhs_tv
-
-    check_rhs lhs_tv_info lhs_tv_lvl = case coreFullView rhs of
-      TyConApp tc tys | isTypeFamilyTyCon tc
-                      , not (isConcreteTyVar lhs_tv)
-        -> -- Special case for  lhs ~ F tys
+    (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of
+         MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl)
+         _ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
+
+    check_rhs = case splitTyConApp_maybe rhs of
+      Just (tc, tys) | isTypeFamilyTyCon tc
+                     , not (isConcreteTyVar lhs_tv)
+        -> -- Special case for  alpha ~ F tys
            -- We don't want to flatten that (F tys)
            do { tys_res <- mapCheck (simple_check lhs_tv_lvl) tys
               ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
@@ -2267,36 +2267,47 @@ checkTypeEq ev eq_rel lhs rhs
   where
     ghci_tv = False
 
-    check_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
-    check_given = case lhs of
-      TyFamLHS _ _ -> checkTyEqRhs ghci_tv refl_tv       check_given_fam_app refl_co
-      TyVarLHS tv  -> checkTyEqRhs ghci_tv (check_tv tv) check_given_fam_app (check_co tv)
-
+    ---------------------- Wanted ------------------
     check_wanted :: TcType -> TcM (PuResult Ct Reduction)
     check_wanted = case lhs of
-       TyFamLHS tc tys -> checkTyEqRhs ghci_tv refl_tv       (check_wanted_fam_app tc tys) refl_co
-       TyVarLHS tv     -> checkTyEqRhs ghci_tv (check_tv tv) (recurseFamApp check_wanted) (check_co tv)
+       TyFamLHS tc tys -> checkTyEqRhs ghci_tv refl_tv (cfa_wanted_fam tc tys) refl_co
+       TyVarLHS tv     -> checkTyEqRhs ghci_tv (check_tv tv) cfa_wanted_tv (check_co tv)
 
     -- Family-application (G tys) in [W] F lhs_tys ~ (...(G tys)...)
-    check_wanted_fam_app :: TyCon -> [TcType]
-                         -> TcType -> TyCon -> [TcType]
-                         -> TcM (PuResult Ct Reduction)
-    check_wanted_fam_app lhs_tc lhs_tys fam_app tc tys
+    cfa_wanted_fam :: TyCon -> [TcType]
+                   -> TcType -> TyCon -> [TcType]
+                   -> TcM (PuResult Ct Reduction)
+    cfa_wanted_fam lhs_tc lhs_tys fam_app tc tys
       | tcEqTyConApps lhs_tc lhs_tys tc tys
       = failCheckWith (occursProblem eq_rel)
       | otherwise
       = recurseFamApp check_wanted fam_app tc tys
 
-    check_given_fam_app fam_app tc tys
+    cfa_wanted_tv fam_app tc tys = recurseFamApp check_wanted fam_app tc tys
+
+    ---------------------- Given ------------------
+    check_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
+    check_given = case lhs of
+      TyFamLHS tc tys -> checkTyEqRhs ghci_tv refl_tv (cfa_given_fam tc tys) refl_co
+      TyVarLHS tv     -> checkTyEqRhs ghci_tv (check_tv tv) cfa_given_tv (check_co tv)
+
+    cfa_given_fam lhs_tc lhs_tys fam_app tc tys
+      | tcEqTyConApps lhs_tc lhs_tys tc tys
+      = break_cycle fam_app
+      | otherwise
+      = recurseFamApp check_given fam_app tc tys
+
+    cfa_given_tv fam_app tc tys
       = -- Try just checking the arguments
         do { tys_res <- mapCheck check_given tys
            ; case tys_res of {
                PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) ;
-               PuFail {}      ->
+               PuFail {}      -> break_cycle fam_app } }
 
-        do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
+    break_cycle fam_app
+      = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
            ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
-                          (unitBag (new_tv, fam_app))) } }}
+                          (unitBag (new_tv, fam_app))) }
                     -- Why reflexive? See Detail (4) of the Note
 
     refl_tv tv = okCheckRefl (mkTyVarTy tv)
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index e65b1aa959..86253a6411 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -2664,9 +2664,8 @@ occursCheckTv lhs_tv occ_tv
 
 uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () ())
 uTypeCheckTouchableTyVarEq lhs_tv rhs
-  | MetaTv { mtv_info = tv_info } <- tcTyVarDetails lhs_tv
   = do { check_result <- checkTyEqRhs False
-                                      (simple_check_tv (isConcreteInfo tv_info))
+                                      simple_check_tv
                                       dont_flatten
                                       (simpleCheckCo lhs_tv True)
                                       rhs
@@ -2676,15 +2675,17 @@ uTypeCheckTouchableTyVarEq lhs_tv rhs
             PuOK redn _   -> assertPpr (isReflCo (reductionCoercion redn))
                                        (ppr lhs_tv $$ ppr rhs $$ ppr redn) $
                              return (PuOK () emptyBag) }
-
-  -- Only called on meta-tyvars
-  | otherwise = pprPanic "uTypeCHeckTouchableTyVarEq" (ppr lhs_tv)
   where
+    lhs_tv_info = case tcTyVarDetails lhs_tv of
+                   MetaTv { mtv_info = tv_info } -> tv_info
+                   _ -> pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
+
     dont_flatten :: TcType -> TyCon -> [TcType] -> TcM (PuResult () Reduction)
     dont_flatten _ _ _ = failCheckWith (cteProblem cteTypeFamily)
      -- See Note [Prevent unification with type families]
 
-    simple_check_tv lhs_tv_is_concrete occ_tv
+    lhs_tv_is_concrete = isConcreteInfo lhs_tv_info
+    simple_check_tv occ_tv
       | occursCheckTv lhs_tv occ_tv
       = failCheckWith insolubleOccursProblem
       | lhs_tv_is_concrete, not (isConcreteTyVar occ_tv)
@@ -2762,14 +2763,18 @@ checkTyEqRhs ghci_tv check_tv flatten_fam_app check_co rhs
                 ; extra_res <- mapCheck go extra_args
                 ; return (mkAppRedns <$> fun_res <*> extra_res) }
 
-      | not (isFamFreeTyCon tc)  -- e.g. S a  where  type S a = F [a]
+      | not (isFamFreeTyCon tc) || isForgetfulSynTyCon tc
+           -- e.g. S a  where  type S a = F [a]
+           --             or   type S a = Int
+           -- ToDo: explain why
       , Just ty' <- coreView ty  -- Only synonyms and type families reply
       = go ty'                   --      False to isFamFreeTyCon
 
-      | otherwise
+      | otherwise  -- Recurse on arguments
       = do { tys_res <- mapCheck go tys
-           ; if | PuFail {} <- tys_res, Just ty' <- coreView ty
-                -> go ty'  -- Expand synonyms on failure
+           ; if | PuFail {} <- tys_res
+                , Just ty' <- coreView ty    -- Expand synonyms on failure
+                -> go ty'                    -- e.g a ~ P a where type P a = Int
                 | not (isTauTyCon tc || ghci_tv)
                 -> failCheckWith impredicativeProblem
                 | otherwise
@@ -2788,20 +2793,20 @@ touchabilityTest given_eq_lvl tv rhs
   = False
 
 -------------------------
--- | checkTopShape checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of
+-- | checkTopShape checks (TYVAR-TV)
 -- Note [Unification preconditions]; returns True if these conditions
 -- are satisfied. But see the Note for other preconditions, too.
 checkTopShape :: MetaInfo -> TcType -> Bool
 checkTopShape info xi
   = case info of
-      CycleBreakerTv -> False
       TyVarTv ->
-        case getTyVar_maybe xi of
+        case getTyVar_maybe xi of   -- Looks through type synonyms
            Nothing -> False
            Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
                         SkolemTv {} -> True
                         RuntimeUnk  -> True
                         MetaTv { mtv_info = TyVarTv } -> True
                         _                             -> False
+      CycleBreakerTv -> False  -- We never unify these
       _ -> True