Commit 2e6cc3d0 authored by Ryan Scott's avatar Ryan Scott

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
parent 75a8349b
......@@ -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,
......
......@@ -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.
************************************************************************
* *
......
......@@ -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',
......
{-# Language PolyKinds #-}
{-# Language TypeApplications #-}
{-# Language ImpredicativeTypes #-}
{-# Language LiberalTypeSynonyms #-}
module T15859 where
......
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
......
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE RankNTypes #-}
module ShouldCompile where
......@@ -11,7 +12,7 @@ foo = error "urk"
-- 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)
......
{-# 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
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’
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
......@@ -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, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment