Compare FunTys as if they were TyConApps.wip/T17674

See Note [Equality on FunTys] in TyCoRep.

Close #17675.
Close #17655, about documentation improvements included in
this patch.
Close #19677, about a further mistake around FunTy.

test cases: typecheck/should_compile/T19677

4 files changed, 70 insertions, 38 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 7d9682582a..8628f75d99 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1808,7 +1808,22 @@ that (a Int) will satisfy (PKTI).
 
 The absence of this caused #14174 and #14520.
 
-The calls to mkAppTyM is the other place we are very careful.
+The calls to mkAppTyM is the other place we are very careful; see Note [mkAppTyM].
+
+Wrinkle around FunTy:
+Note that the PKTI does *not* guarantee anything about the shape of FunTys.
+Specifically, when we have (FunTy vis mult arg res), it should be the case
+that arg :: TYPE rr1 and res :: TYPE rr2, for some rr1 and rr2. However, we
+might not have this. Example: if the user writes (a -> b), then we might
+invent a :: kappa1 and b :: kappa2. We soon will check whether kappa1 ~ TYPE rho1
+(for some rho1), and that will lead to kappa1 := TYPE rho1 (ditto for kappa2).
+However, when we build the FunTy, we might not have zonked `a`, and so the
+FunTy will be built without being able to purely extract the RuntimeReps.
+
+Because the PKTI does not guarantee that the RuntimeReps are available in a FunTy,
+we must be aware of this when splitting: splitTyConApp and splitAppTy will *not*
+split a FunTy if the RuntimeReps are not available. See also Note [Decomposing FunTy]
+in GHC.Tc.Solver.Canonical.
 
 Note [mkAppTyM]
 ~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index e8c4ee82e2..cdb86b92e2 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -914,7 +914,6 @@ track whether or not we've already rewritten.
 It is conceivable to do a better job at tracking whether or not a type
 is rewritten, but this is left as future work. (Mar '15)
 
-
 Note [Decomposing FunTy]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 can_eq_nc' may attempt to decompose a FunTy that is un-zonked.  This
@@ -1291,8 +1290,8 @@ zonk_eq_types = go
         split2 = tcSplitFunTy_maybe ty2
 
     go ty1 ty2
-      | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1
-      , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2
+      | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
+      , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
       = if tc1 == tc2 && tys1 `equalLength` tys2
           -- Crucial to check for equal-length args, because
           -- we cannot assume that the two args to 'go' have
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 82c6c580a4..3f2f8f35ce 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -41,6 +41,8 @@ import GHC.Exts (oneShot)
 import Control.Monad
 import GHC.Utils.Monad ( zipWith3M )
 import Data.List.NonEmpty ( NonEmpty(..) )
+import Control.Applicative (liftA3)
+import GHC.Builtin.Types.Prim (tYPETyCon)
 
 {-
 ************************************************************************
@@ -470,28 +472,28 @@ rewrite_args_slow binders inner_ki fvs roles tys
 -- a Derived rewriting a Derived. The solution would be to generate evidence for
 -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
 -- Note [No derived kind equalities]
-  = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
+  = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True)
                                         roles tys
        ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
   where
-    {-# INLINE fl #-}
-    fl :: Bool   -- must we ensure to produce a real coercion here?
+    {-# INLINE rw #-}
+    rw :: Bool   -- must we ensure to produce a real coercion here?
                  -- see comment at top of function
        -> Role -> Type -> RewriteM Reduction
-    fl True  r ty = noBogusCoercions $ fl1 r ty
-    fl False r ty =                    fl1 r ty
+    rw True  r ty = noBogusCoercions $ rw1 r ty
+    rw False r ty =                    rw1 r ty
 
-    {-# INLINE fl1 #-}
-    fl1 :: Role -> Type -> RewriteM Reduction
-    fl1 Nominal ty
+    {-# INLINE rw1 #-}
+    rw1 :: Role -> Type -> RewriteM Reduction
+    rw1 Nominal ty
       = setEqRel NomEq $
         rewrite_one ty
 
-    fl1 Representational ty
+    rw1 Representational ty
       = setEqRel ReprEq $
         rewrite_one ty
 
-    fl1 Phantom ty
+    rw1 Phantom ty
     -- See Note [Phantoms in the rewriter]
       = do { ty <- liftTcS $ zonkTcType ty
            ; return $ mkReflRedn Phantom ty }
@@ -533,9 +535,35 @@ rewrite_one (TyConApp tc tys)
 rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
   = do { arg_redn <- rewrite_one ty1
        ; res_redn <- rewrite_one ty2
-       ; w_redn <- setEqRel NomEq $ rewrite_one mult
+
+        -- Important: look at the *reduced* type, so that any unzonked variables
+        -- in kinds are gone and the getRuntimeRep succeeds.
+        -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical.
+       ; let arg_rep = getRuntimeRep (reductionReducedType arg_redn)
+             res_rep = getRuntimeRep (reductionReducedType res_redn)
+
+       ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $
+           liftA3 (,,) (rewrite_one mult)
+                       (rewrite_one arg_rep)
+                       (rewrite_one res_rep)
        ; role <- getRole
-       ; return $ mkFunRedn role vis w_redn arg_redn res_redn }
+
+       ; let arg_rep_co = reductionCoercion arg_rep_redn
+                -- :: arg_rep ~ arg_rep_xi
+             arg_ki_co  = mkTyConAppCo Nominal tYPETyCon [arg_rep_co]
+                -- :: TYPE arg_rep ~ TYPE arg_rep_xi
+             casted_arg_redn = mkCoherenceRightRedn role arg_redn arg_ki_co
+                -- :: ty1 ~> arg_xi |> arg_ki_co
+
+             res_rep_co = reductionCoercion res_rep_redn
+             res_ki_co  = mkTyConAppCo Nominal tYPETyCon [res_rep_co]
+             casted_res_redn = mkCoherenceRightRedn role res_redn res_ki_co
+
+          -- We must rewrite the representations, because that's what would
+          -- be done if we used TyConApp instead of FunTy. These rewritten
+          -- representations are seen only in casts of the arg and res, below.
+          -- Forgetting this caused #19677.
+       ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn }
 
 rewrite_one ty@(ForAllTy {})
 -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 367922e3e5..d878ccc75a 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -625,6 +625,10 @@ EQUAL TO, but we'd need to think carefully about
 But in fact (GivenInv) is automatically true, so we're adhering to
 it for now.  See #18929.
 
+* If a tyvar tv has level n, then the levels of all variables free
+  in tv's kind are <= n. Consequence: if tv is untouchable, so are
+  all variables in tv's kind.
+
 Note [WantedInv]
 ~~~~~~~~~~~~~~~~
 Why is WantedInv important?  Consider this implication, where
@@ -1591,6 +1595,7 @@ tc_eq_type :: Bool          -- ^ True <=> do not expand type synonyms
            -> Type -> Type
            -> Bool
 -- Flags False, False is the usual setting for tc_eq_type
+-- See Note [Computing equality on types] in Type
 tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
   = go orig_env orig_ty1 orig_ty2
   where
@@ -1620,10 +1625,14 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
     -- Make sure we handle all FunTy cases since falling through to the
     -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
     -- kind variable, which causes things to blow up.
+    -- See Note [Equality on FunTys] in GHC.Core.TyCo.Rep: we must check
+    -- kinds here
     go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
-      = go env w1 w2 && go env arg1 arg2 && go env res1 res2
-    go env ty (FunTy _ w arg res) = eqFunTy env w arg res ty
-    go env (FunTy _ w arg res) ty = eqFunTy env w arg res ty
+      = kinds_eq && go env arg1 arg2 && go env res1 res2 && go env w1 w2
+      where
+        kinds_eq | vis_only  = True
+                 | otherwise = go env (typeKind arg1) (typeKind arg2) &&
+                               go env (typeKind res1) (typeKind res2)
 
       -- See Note [Equality on AppTys] in GHC.Core.Type
     go env (AppTy s1 t1)        ty2
@@ -1658,25 +1667,6 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
 
     orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
 
-    -- @eqFunTy w arg res ty@ is True when @ty@ equals @FunTy w arg res@. This is
-    -- sometimes hard to know directly because @ty@ might have some casts
-    -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
-    -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
-    -- res is unzonked. Thus this function, which handles this
-    -- corner case.
-    eqFunTy :: RnEnv2 -> Mult -> Type -> Type -> Type -> Bool
-               -- Last arg is /not/ FunTy
-    eqFunTy env w arg res ty@(AppTy{}) = get_args ty []
-      where
-        get_args :: Type -> [Type] -> Bool
-        get_args (AppTy f x)       args = get_args f (x:args)
-        get_args (CastTy t _)      args = get_args t args
-        get_args (TyConApp tc tys) args
-          | tc == funTyCon
-          , [w', _, _, arg', res'] <- tys ++ args
-          = go env w w' && go env arg arg' && go env res res'
-        get_args _ _    = False
-    eqFunTy _ _ _ _ _   = False
 {-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
 
 {- Note [Typechecker equality vs definitional equality]