Commit e1b5a117 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix a nasty bug in piResultTys

I was failing to instantiate vigorously enough in Type.piResultTys
and in the very similar function ToIface.toIfaceAppArgsX

This caused Trac #15428.  The fix is easy.

See Note [Care with kind instantiation] in Type.hs
parent f0d27f51
......@@ -305,10 +305,10 @@ toIfaceAppArgsX fr kind ty_args
go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
= IA_Vis (toIfaceTypeX fr t) (go env res ts)
go env (TyVarTy tv) ts
| Just ki <- lookupTyVar env tv = go env ki ts
go env kind (t:ts) = WARN( True, ppr kind $$ ppr ty_args )
IA_Vis (toIfaceTypeX fr t) (go env kind ts) -- Ill-kinded
go env ty ts = ASSERT2( not (isEmptyTCvSubst env)
, ppr kind $$ ppr ty_args )
go (zapTCvSubst env) (substTy env ty) ts
-- See Note [Care with kind instantiation] in Type.hs
tidyToIfaceType :: TidyEnv -> Type -> IfaceType
tidyToIfaceType env ty = toIfaceType (tidyType env ty)
......
......@@ -1038,13 +1038,12 @@ piResultTys ty orig_args@(arg:args)
| ForAllTy (TvBndr tv _) res <- ty
= go (extendVarEnv tv_env tv arg) res args
| TyVarTy tv <- ty
, Just ty' <- lookupVarEnv tv_env tv
-- Deals with piResultTys (forall a. a) [forall b.b, Int]
= piResultTys ty' all_args
| otherwise
= pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
| otherwise -- See Note [Care with kind instantiation]
= ASSERT2( not (isEmptyVarEnv tv_env)
, ppr ty $$ ppr orig_args $$ ppr all_args )
go emptyTvSubstEnv
(substTy (mkTvSubst in_scope tv_env) ty)
all_args
applyTysX :: [TyVar] -> Type -> [Type] -> Type
-- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
......@@ -1058,7 +1057,35 @@ applyTysX tvs body_ty arg_tys
pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
n_tvs = length tvs
{-
{- Note [Care with kind instantiation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
T :: forall k. k
and we are finding the kind of
T (forall b. b -> b) * Int
Then
T (forall b. b->b) :: k[ k :-> forall b. b->b]
:: forall b. b -> b
So
T (forall b. b->b) * :: (b -> b)[ b :-> *]
:: * -> *
In other words wwe must intantiate the forall!
Similarly (Trac #154218)
S :: forall k f. k -> f k
and we are finding the kind of
S * (* ->) Int Bool
We have
S * (* ->) :: (k -> f k)[ k :-> *, f :-> (* ->)]
:: * -> * -> *
So again we must instantiate.
The same thing happens in ToIface.toIfaceAppArgsX.
---------------------------------------------------------------------
TyConApp
~~~~~~~~
......
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T15428 where
data Flurmp
type family Pure (x :: a) :: f a
type T = Pure Flurmp Flurmp
......@@ -642,3 +642,4 @@ def onlyHsParLocs(x):
test('T15242', normalise_errmsg_fun(onlyHsParLocs), compile, [''])
test('T15431', normal, compile, [''])
test('T15431a', normal, compile, [''])
test('T15428', normal, compile, [''])
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