Fix #15954 by rejigging check_type's order

Summary:
Previously, `check_type` (which catches illegal uses of
unsaturated type synonyms without enabling `LiberalTypeSynonyms`,
among other things) always checks for uses of polytypes before
anything else. There is a problem with this plan, however:
checking for polytypes requires decomposing `forall`s and other
invisible arguments, an action which itself expands type synonyms!
Therefore, if we have something like:

```lang=haskell
type A a = Int
type B (a :: Type -> Type) = forall x. x -> x
type C = B A
```

Then when checking `B A`, `A` will get expanded to `forall x. x -> x`
before `check_type` has an opportunity to realize that `A` is an
unsaturated type synonym! This is the root cause of #15954.

This patch fixes the issue by moving the case of `check_type` that
detects polytypes to be //after// the case that checks for
`TyConApp`s. That way, the `TyConApp` case will properly flag things
like the unsaturated use of `A` in the example above before we ever
attempt to check for polytypes.

Test Plan: make test TEST=T15954

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15954

Differential Revision: https://phabricator.haskell.org/D5402

3 files changed, 59 insertions, 19 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 1e596baa09..df1ec91cf2 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -64,7 +64,7 @@ module TcType (
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
   tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe,
-  tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
+  tcRepSplitTyConApp, tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
   tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
   tcRepGetNumAppTys,
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 560b83db12..a3f4e2f20b 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -458,6 +458,26 @@ check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- Rank 0 means no for-alls anywhere
 
+check_type _ _ _ (TyVarTy _) = return ()
+
+check_type env ctxt rank (AppTy ty1 ty2)
+  = do  { check_type env ctxt rank ty1
+        ; check_arg_type env ctxt rank ty2 }
+
+check_type env ctxt rank ty@(TyConApp tc tys)
+  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
+  = check_syn_tc_app env ctxt rank ty tc tys
+  | isUnboxedTupleTyCon tc = check_ubx_tuple  env ctxt      ty    tys
+  | otherwise              = mapM_ (check_arg_type env ctxt rank) tys
+
+check_type _ _ _ (LitTy {}) = return ()
+
+check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
+
+-- Check for rank-n types, such as (forall x. x -> x) or (Show x => x).
+--
+-- Critically, this case must come *after* the case for TyConApp.
+-- See Note [Liberal type synonyms].
 check_type env ctxt rank ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
@@ -491,28 +511,12 @@ check_type env ctxt rank ty
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
 
-check_type _ _ _ (TyVarTy _) = return ()
-
 check_type env ctxt rank (FunTy arg_ty res_ty)
   = do  { check_type env ctxt arg_rank arg_ty
         ; check_type env ctxt res_rank res_ty }
   where
     (arg_rank, res_rank) = funArgResRank rank
 
-check_type env ctxt rank (AppTy ty1 ty2)
-  = do  { check_type env ctxt rank ty1
-        ; check_arg_type env ctxt rank ty2 }
-
-check_type env ctxt rank ty@(TyConApp tc tys)
-  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-  = check_syn_tc_app env ctxt rank ty tc tys
-  | isUnboxedTupleTyCon tc = check_ubx_tuple  env ctxt      ty    tys
-  | otherwise              = mapM_ (check_arg_type env ctxt rank) tys
-
-check_type _ _ _ (LitTy {}) = return ()
-
-check_type env ctxt rank (CastTy ty _) = check_type env ctxt rank ty
-
 check_type _ _ _ ty = pprPanic "check_type" (ppr ty)
 
 ----------------------------------------
@@ -537,7 +541,10 @@ check_syn_tc_app env ctxt rank ty tc tys
 
           else  -- In the liberal case (only for closed syns), expand then check
           case tcView ty of
-             Just ty' -> check_type env ctxt rank ty'
+             Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
+                             err_ctxt = text "In the expansion of type synonym"
+                                        <+> quotes (ppr syn_tc)
+                         in addErrCtxt err_ctxt $ check_type env ctxt rank ty'
              Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
 
   | GhciCtxt <- ctxt  -- Accept under-saturated type synonyms in
@@ -662,6 +669,31 @@ If we do both, we get exponential behaviour!!
   type TIACons4 t x = TIACons2 t (TIACons2 t x)
   type TIACons7 t x = TIACons4 t (TIACons3 t x)
 
+The order in which you do validity checking is also somewhat delicate. Consider
+the `check_type` function, which drives the validity checking for unsaturated
+uses of type synonyms. There is a special case for rank-n types, such as
+(forall x. x -> x) or (Show x => x), since those require at least one language
+extension to use. It used to be the case that this case came before every other
+case, but this can lead to bugs. Imagine you have this scenario (from #15954):
+
+  type A a = Int
+  type B (a :: Type -> Type) = forall x. x -> x
+  type C = B A
+
+If the rank-n case came first, then in the process of checking for `forall`s
+or contexts, we would expand away `B A` to `forall x. x -> x`. This is because
+the functions that split apart `forall`s/contexts
+(tcSplitForAllVarBndrs/tcSplitPhiTy) expand type synonyms! If `B A` is expanded
+away to `forall x. x -> x` before the actually validity checks occur, we will
+have completely obfuscated the fact that we had an unsaturated application of
+the `A` type synonym.
+
+We have since learned from our mistakes and now put this rank-n case /after/
+the case for TyConApp, which ensures that an unsaturated `A` TyConApp will be
+caught properly. But be careful! We can't make the rank-n case /last/ either,
+as the FunTy case must came after the rank-n case. Otherwise, something like
+(Eq a => Int) would be treated as a function type (FunTy), which just
+wouldn't do.
 
 ************************************************************************
 *                                                                      *
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index b4c29ce9fb..e489551aa4 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -32,7 +32,7 @@ module Type (
         tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
         tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
         splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
-        tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
+        tcRepSplitTyConApp_maybe, tcRepSplitTyConApp, tcSplitTyConApp_maybe,
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
 
@@ -798,6 +798,14 @@ tcRepSplitTyConApp_maybe (FunTy arg res)
 tcRepSplitTyConApp_maybe _
   = Nothing
 
+-- | Like 'tcSplitTyConApp' but doesn't look through type synonyms.
+tcRepSplitTyConApp :: HasCallStack => Type -> (TyCon, [Type])
+-- Defined here to avoid module loops between Unify and TcType.
+tcRepSplitTyConApp ty =
+  case tcRepSplitTyConApp_maybe ty of
+    Just stuff -> stuff
+    Nothing    -> pprPanic "tcRepSplitTyConApp" (ppr ty)
+
 -------------
 splitAppTy :: Type -> (Type, Type)
 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',