Allow multiple case branches to have a higher rank type

As #18412 points out, it should be OK for multiple case alternatives
to have a higher rank type, provided they are all the same.

This patch implements that change.  It sweeps away
GHC.Tc.Gen.Match.tauifyMultipleBranches, and friends, replacing it
with an enhanced version of fillInferResult.

The basic change to fillInferResult is to permit the case in which
another case alternative has already filled in the result; and in
that case simply unify.  It's very simple actually.

See the new Note [fillInferResult] in TcMType

Other refactoring:

- Move all the InferResult code to one place, in GHC.Tc.Utils.TcMType
  (previously some of it was in Unify)

- Move tcInstType and friends from TcMType to Instantiate, where it
  more properly belongs.  (TCMType was getting very long.)

1 files changed, 42 insertions, 209 deletions

diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 5d7afcf057..145520045b 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -61,7 +61,6 @@ import GHC.Types.Name( isSystemName )
 import GHC.Tc.Utils.Instantiate
 import GHC.Core.TyCon
 import GHC.Builtin.Types
-import GHC.Builtin.Types.Prim( tYPE )
 import GHC.Types.Var as Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -571,10 +570,51 @@ tcSubTypeNC :: CtOrigin       -- Used when instantiating
             -> TcM HsWrapper
 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
   = case res_ty of
-      Infer inf_res     -> instantiateAndFillInferResult inst_orig ty_actual inf_res
       Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
                                        ty_actual ty_expected
 
+      Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
+                                   -- See Note [Instantiation of InferResult]
+                          ; co <- fillInferResult rho inf_res
+                          ; return (mkWpCastN co <.> wrap) }
+
+{- Note [Instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We now always instantiate before filling in InferResult, so that
+the result is a TcRhoType: see #17173 for discussion.
+
+For example:
+
+1. Consider
+    f x = (*)
+   We want to instantiate the type of (*) before returning, else we
+   will infer the type
+     f :: forall {a}. a -> forall b. Num b => b -> b -> b
+   This is surely confusing for users.
+
+   And worse, the monomorphism restriction won't work properly. The MR is
+   dealt with in simplifyInfer, and simplifyInfer has no way of
+   instantiating. This could perhaps be worked around, but it may be
+   hard to know even when instantiation should happen.
+
+2. Another reason.  Consider
+       f :: (?x :: Int) => a -> a
+       g y = let ?x = 3::Int in f
+   Here want to instantiate f's type so that the ?x::Int constraint
+   gets discharged by the enclosing implicit-parameter binding.
+
+3. Suppose one defines plus = (+). If we instantiate lazily, we will
+   infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
+   restriction compels us to infer
+      plus :: Integer -> Integer -> Integer
+   (or similar monotype). Indeed, the only way to know whether to apply
+   the monomorphism restriction at all is to instantiate
+
+There is one place where we don't want to instantiate eagerly,
+namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
+command. See Note [Implementing :type] in GHC.Tc.Module.
+-}
+
 ---------------
 tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 -- External entry point, but no ExpTypes on either side
@@ -768,213 +808,6 @@ tcEqMult origin w_actual w_expected = do
   ; coercion <- uType TypeLevel origin w_actual w_expected
   ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
 
-{- **********************************************************************
-%*                                                                      *
-            ExpType functions: tcInfer, instantiateAndFillInferResult
-%*                                                                      *
-%********************************************************************* -}
-
--- | Infer a type using a fresh ExpType
--- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
-tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInfer tc_check
-  = do { res_ty <- newInferExpType
-       ; result <- tc_check res_ty
-       ; res_ty <- readExpType res_ty
-       ; return (result, res_ty) }
-
-instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = instantiateAndFillInferResult t1 t2
---    => wrap :: t1 ~> t2
--- See Note [Instantiation of InferResult]
-instantiateAndFillInferResult orig ty inf_res
-  = do { (wrap, rho) <- topInstantiate orig ty
-       ; co <- fillInferResult rho inf_res
-       ; return (mkWpCastN co <.> wrap) }
-
-fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fillInferResult t1 t2
---    => wrap :: t1 ~> t2
-fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
-                            , ir_ref = ref })
-  = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
-
-       ; traceTc "Filling ExpType" $
-         ppr u <+> text ":=" <+> ppr ty_to_fill_with
-
-       ; when debugIsOn (check_hole ty_to_fill_with)
-
-       ; writeTcRef ref (Just ty_to_fill_with)
-
-       ; return ty_co }
-  where
-    check_hole ty   -- Debug check only
-      = do { let ty_lvl = tcTypeLevel ty
-           ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
-                       ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
-                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
-           ; cts <- readTcRef ref
-           ; case cts of
-               Just already_there -> pprPanic "writeExpType"
-                                       (vcat [ ppr u
-                                             , ppr ty
-                                             , ppr already_there ])
-               Nothing -> return () }
-
-{- Note [Instantiation of InferResult]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We now always instantiate before filling in InferResult, so that
-the result is a TcRhoType: see #17173 for discussion.
-
-For example:
-
-1. Consider
-    f x = (*)
-   We want to instantiate the type of (*) before returning, else we
-   will infer the type
-     f :: forall {a}. a -> forall b. Num b => b -> b -> b
-   This is surely confusing for users.
-
-   And worse, the monomorphism restriction won't work properly. The MR is
-   dealt with in simplifyInfer, and simplifyInfer has no way of
-   instantiating. This could perhaps be worked around, but it may be
-   hard to know even when instantiation should happen.
-
-2. Another reason.  Consider
-       f :: (?x :: Int) => a -> a
-       g y = let ?x = 3::Int in f
-   Here want to instantiate f's type so that the ?x::Int constraint
-   gets discharged by the enclosing implicit-parameter binding.
-
-3. Suppose one defines plus = (+). If we instantiate lazily, we will
-   infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
-   restriction compels us to infer
-      plus :: Integer -> Integer -> Integer
-   (or similar monotype). Indeed, the only way to know whether to apply
-   the monomorphism restriction at all is to instantiate
-
-There is one place where we don't want to instantiate eagerly,
-namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
-command. See Note [Implementing :type] in GHC.Tc.Module.
-
--}
-
-{- *********************************************************************
-*                                                                      *
-              Promoting types
-*                                                                      *
-********************************************************************* -}
-
-promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
--- See Note [Promoting a type]
--- promoteTcType level ty = (co, ty')
---   * Returns ty'  whose max level is just 'level'
---             and  whose kind is ~# to the kind of 'ty'
---             and  whose kind has form TYPE rr
---   * and co :: ty ~ ty'
---   * and emits constraints to justify the coercion
-promoteTcType dest_lvl ty
-  = do { cur_lvl <- getTcLevel
-       ; if (cur_lvl `sameDepthAs` dest_lvl)
-         then dont_promote_it
-         else promote_it }
-  where
-    promote_it :: TcM (TcCoercion, TcType)
-    promote_it  -- Emit a constraint  (alpha :: TYPE rr) ~ ty
-                -- where alpha and rr are fresh and from level dest_lvl
-      = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
-           ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
-           ; let eq_orig = TypeEqOrigin { uo_actual   = ty
-                                        , uo_expected = prom_ty
-                                        , uo_thing    = Nothing
-                                        , uo_visible  = False }
-
-           ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
-           ; return (co, prom_ty) }
-
-    dont_promote_it :: TcM (TcCoercion, TcType)
-    dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
-      = do { res_kind <- newOpenTypeKind
-           ; let ty_kind = tcTypeKind ty
-                 kind_orig = TypeEqOrigin { uo_actual   = ty_kind
-                                          , uo_expected = res_kind
-                                          , uo_thing    = Nothing
-                                          , uo_visible  = False }
-           ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
-           ; let co = mkTcGReflRightCo Nominal ty ki_co
-           ; return (co, ty `mkCastTy` ki_co) }
-
-{- Note [Promoting a type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#12427)
-
-  data T where
-    MkT :: (Int -> Int) -> a -> T
-
-  h y = case y of MkT v w -> v
-
-We'll infer the RHS type with an expected type ExpType of
-  (IR { ir_lvl = l, ir_ref = ref, ... )
-where 'l' is the TcLevel of the RHS of 'h'.  Then the MkT pattern
-match will increase the level, so we'll end up in tcSubType, trying to
-unify the type of v,
-  v :: Int -> Int
-with the expected type.  But this attempt takes place at level (l+1),
-rightly so, since v's type could have mentioned existential variables,
-(like w's does) and we want to catch that.
-
-So we
-  - create a new meta-var alpha[l+1]
-  - fill in the InferRes ref cell 'ref' with alpha
-  - emit an equality constraint, thus
-        [W] alpha[l+1] ~ (Int -> Int)
-
-That constraint will float outwards, as it should, unless v's
-type mentions a skolem-captured variable.
-
-This approach fails if v has a higher rank type; see
-Note [Promotion and higher rank types]
-
-
-Note [Promotion and higher rank types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
-then we'd emit an equality
-        [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
-which will sadly fail because we can't unify a unification variable
-with a polytype.  But there is nothing really wrong with the program
-here.
-
-We could just about solve this by "promote the type" of v, to expose
-its polymorphic "shape" while still leaving constraints that will
-prevent existential escape.  But we must be careful!  Exposing
-the "shape" of the type is precisely what we must NOT do under
-a GADT pattern match!  So in this case we might promote the type
-to
-        (forall a. a->a) -> alpha[l+1]
-and emit the constraint
-        [W] alpha[l+1] ~ Int
-Now the promoted type can fill the ref cell, while the emitted
-equality can float or not, according to the usual rules.
-
-But that's not quite right!  We are exposing the arrow! We could
-deal with that too:
-        (forall a. mu[l+1] a a) -> alpha[l+1]
-with constraints
-        [W] alpha[l+1] ~ Int
-        [W] mu[l+1] ~ (->)
-Here we abstract over the '->' inside the forall, in case that
-is subject to an equality constraint from a GADT match.
-
-Note that we kept the outer (->) because that's part of
-the polymorphic "shape".  And because of impredicativity,
-GADT matches can't give equalities that affect polymorphic
-shape.
-
-This reasoning just seems too complicated, so I decided not
-to do it.  These higher-rank notes are just here to record
-the thinking.
--}
 
 {- *********************************************************************
 *                                                                      *