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

10 files changed, 90 insertions, 25 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',
diff --git a/testsuite/tests/dependent/should_fail/T15859.hs b/testsuite/tests/dependent/should_fail/T15859.hs
index e8ffdf4ae2..e7adc5fc98 100644
--- a/testsuite/tests/dependent/should_fail/T15859.hs
+++ b/testsuite/tests/dependent/should_fail/T15859.hs
@@ -1,6 +1,7 @@
 {-# Language PolyKinds          #-}
 {-# Language TypeApplications   #-}
 {-# Language ImpredicativeTypes #-}
+{-# Language LiberalTypeSynonyms #-}
 
 module T15859 where
 
diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr
index e4794048b7..c4dc1ef086 100644
--- a/testsuite/tests/dependent/should_fail/T15859.stderr
+++ b/testsuite/tests/dependent/should_fail/T15859.stderr
@@ -1,5 +1,5 @@
 
-T15859.hs:13:5: error:
+T15859.hs:14:5: error:
     • Cannot apply expression of type ‘forall k -> k -> *’
       to a visible type argument ‘Int’
     • In the expression: (undefined :: KindOf A) @Int
diff --git a/testsuite/tests/typecheck/should_compile/tc149.hs b/testsuite/tests/typecheck/should_compile/tc149.hs
index 5813604bc3..a788fbfb96 100644
--- a/testsuite/tests/typecheck/should_compile/tc149.hs
+++ b/testsuite/tests/typecheck/should_compile/tc149.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE LiberalTypeSynonyms #-}
 {-# LANGUAGE RankNTypes #-}
 
 module ShouldCompile where
@@ -8,10 +9,10 @@ type Id x = x
 foo :: Generic Id Id
 foo = error "urk"
 
--- The point here is that we instantiate "i" and "o" 
+-- The point here is that we instantiate "i" and "o"
 -- with a partially applied type synonym.  This is
 -- OK in GHC because we check type validity only *after*
--- expanding type synonyms.
+-- expanding type synonyms (with LiberalTypeSynonyms enabled).
 --
 -- However, a bug in GHC 5.03-Feb02 made this break a
 -- type invariant (see Type.mkAppTy)
diff --git a/testsuite/tests/typecheck/should_fail/T15954.hs b/testsuite/tests/typecheck/should_fail/T15954.hs
new file mode 100644
index 0000000000..7b63d35a33
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15954.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+module T15954 where
+
+import Data.Kind
+
+type A a = Int
+type B1 (a :: Type -> Type) = forall x. x -> x
+type C1 = B1 A
+
+data NonShow
+type B2 (a :: Type -> Type) = Show NonShow => Int
+type C2 = B2 A
diff --git a/testsuite/tests/typecheck/should_fail/T15954.stderr b/testsuite/tests/typecheck/should_fail/T15954.stderr
new file mode 100644
index 0000000000..53146b770b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15954.stderr
@@ -0,0 +1,8 @@
+
+T15954.hs:10:1: error:
+    • The type synonym ‘A’ should have 1 argument, but has been given none
+    • In the type synonym declaration for ‘C1’
+
+T15954.hs:14:1: error:
+    • The type synonym ‘A’ should have 1 argument, but has been given none
+    • In the type synonym declaration for ‘C2’
diff --git a/testsuite/tests/typecheck/should_fail/T7809.stderr b/testsuite/tests/typecheck/should_fail/T7809.stderr
index 8e5eea9a52..9ec32b3ff6 100644
--- a/testsuite/tests/typecheck/should_fail/T7809.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7809.stderr
@@ -1,6 +1,6 @@
 
 T7809.hs:8:8: error:
-    • Illegal polymorphic type: PolyId
+    • Illegal polymorphic type: forall a. a -> a
       GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        foo :: F PolyId
+    • In the expansion of type synonym ‘PolyId’
+      In the type signature: foo :: F PolyId
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e033f176fa..7ca05e68db 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -489,4 +489,5 @@ test('T15629', normal, compile_fail, [''])
 test('T15767', normal, compile_fail, [''])
 test('T15648', [extra_files(['T15648a.hs'])], multimod_compile_fail, ['T15648', '-v0 -fprint-equality-relations'])
 test('T15796', normal, compile_fail, [''])
+test('T15954', normal, compile_fail, [''])
 test('T15962', normal, compile_fail, [''])