Commit 77bb0927 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Re-add FunTy (big patch)

With TypeInType Richard combined ForAllTy and FunTy, but that was often
awkward, and yielded little benefit becuase in practice the two were
always treated separately.  This patch re-introduces FunTy.  Specfically

* New type
    data TyVarBinder = TvBndr TyVar VisibilityFlag
  This /always/ has a TyVar it.  In many places that's just what
  what we want, so there are /lots/ of TyBinder -> TyVarBinder changes

* TyBinder still exists:
    data TyBinder = Named TyVarBinder | Anon Type

* data Type = ForAllTy TyVarBinder Type
            | FunTy Type Type
            |  ....

There are a LOT of knock-on changes, but they are all routine.

The Haddock submodule needs to be updated too
parent e33ca0e5
......@@ -30,8 +30,8 @@ module DataCon (
dataConRepType, dataConSig, dataConInstSig, dataConFullSig,
dataConName, dataConIdentity, dataConTag, dataConTyCon,
dataConOrigTyCon, dataConUserType,
dataConUnivTyVars, dataConUnivTyBinders,
dataConExTyVars, dataConExTyBinders,
dataConUnivTyVars, dataConUnivTyVarBinders,
dataConExTyVars, dataConExTyVarBinders,
dataConAllTyVars,
dataConEqSpec, dataConTheta,
dataConStupidTheta,
......@@ -307,14 +307,10 @@ data DataCon
-- Universally-quantified type vars [a,b,c]
-- INVARIANT: length matches arity of the dcRepTyCon
-- INVARIANT: result type of data con worker is exactly (T a b c)
dcUnivTyVars :: [TyVar], -- Two linked fields
dcUnivTyBinders :: [TyBinder], -- see Note [TyBinders in DataCons]
dcUnivTyVars :: [TyVarBinder],
-- Existentially-quantified type vars [x,y]
dcExTyVars :: [TyVar], -- Two linked fields
dcExTyBinders :: [TyBinder], -- see Note [TyBinders in DataCons]
dcExTyVars :: [TyVarBinder],
-- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
-- Reason: less confusing, and easier to generate IfaceSyn
......@@ -416,38 +412,18 @@ data DataCon
}
{- Note [TyBinders in DataCons]
{- Note [TyVarBinders in DataCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
DataCons and PatSyns store their universal and existential type
variables in a pair of fields, e.g.
dcUnivTyVars :: [TyVar],
dcUnivTyBinders :: [TyBinder],
and similarly dcExTyVars/dcExTyVarBinders
Of these, the former is always redundant:
dcUnivTyVars = [ tv | Named tv _ <- dcUnivTyBinders ]
Specifically:
* The two fields correspond 1-1
For the TyVarBinders in a DataCon and PatSyn:
* Each TyBinder a Named (no Anons)
* The TyVar in each TyBinder is the same as the TyVar in
the corresponding tyvar in the TyVars list.
* Each Visibilty flag (va, vb, etc) is Invisible or Specified.
* Each Visibilty flag is Invisible or Specified.
None are Visible. (A DataCon is a term-level function; see
Note [No Visible TyBinder in terms] in TyCoRep.)
Why store these fields redundantly? Purely convenience. In most
places in GHC, it's just the TyVars that are needed, so that's what's
returned from, say, dataConFullSig.
Why do we need the TyBinders? So that we can construct the right
type for the DataCon with its foralls attributed the correce visiblity.
That in turn governs whether you can use visible type application
at a call of the data constructor.
Why do we need the TyVarBinders, rather than just the TyVars? So that
we can construct the right type for the DataCon with its foralls
attributed the correce visiblity. That in turn governs whether you
can use visible type application at a call of the data constructor.
-}
data DataConRep
......@@ -571,11 +547,11 @@ substEqSpec subst (EqSpec tv ty)
tv' = getTyVar "substEqSpec" (substTyVar subst tv)
-- | Filter out any TyBinders mentioned in an EqSpec
filterEqSpec :: [EqSpec] -> [TyBinder] -> [TyBinder]
filterEqSpec :: [EqSpec] -> [TyVarBinder] -> [TyVarBinder]
filterEqSpec eq_spec
= filter not_in_eq_spec
where
not_in_eq_spec bndr = let var = binderVar "filterEqSpec" bndr in
not_in_eq_spec bndr = let var = binderVar bndr in
all (not . (== var) . eqSpecTyVar) eq_spec
instance Outputable EqSpec where
......@@ -761,8 +737,8 @@ mkDataCon :: Name
-> [HsSrcBang] -- ^ Strictness/unpack annotations, from user
-> [FieldLabel] -- ^ Field labels for the constructor,
-- if it is a record, otherwise empty
-> [TyVar] -> [TyBinder] -- ^ Universals. See Note [TyBinders in DataCons]
-> [TyVar] -> [TyBinder] -- ^ Existentials.
-> [TyVarBinder] -- ^ Universals. See Note [TyVarBinders in DataCons]
-> [TyVarBinder] -- ^ Existentials.
-- (These last two must be Named and Invisible/Specified)
-> [EqSpec] -- ^ GADT equalities
-> ThetaType -- ^ Theta-type occuring before the arguments proper
......@@ -780,7 +756,7 @@ mkDataCon :: Name
mkDataCon name declared_infix prom_info
arg_stricts -- Must match orig_arg_tys 1-1
fields
univ_tvs univ_bndrs ex_tvs ex_bndrs
univ_tvs ex_tvs
eq_spec theta
orig_arg_tys orig_res_ty rep_info rep_tycon
stupid_theta work_id rep
......@@ -797,8 +773,8 @@ mkDataCon name declared_infix prom_info
is_vanilla = null ex_tvs && null eq_spec && null theta
con = MkData {dcName = name, dcUnique = nameUnique name,
dcVanilla = is_vanilla, dcInfix = declared_infix,
dcUnivTyVars = univ_tvs, dcUnivTyBinders = univ_bndrs,
dcExTyVars = ex_tvs, dcExTyBinders = ex_bndrs,
dcUnivTyVars = univ_tvs,
dcExTyVars = ex_tvs,
dcEqSpec = eq_spec,
dcOtherTheta = theta,
dcStupidTheta = stupid_theta,
......@@ -819,18 +795,18 @@ mkDataCon name declared_infix prom_info
tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
rep_arg_tys = dataConRepArgTys con
rep_ty = mkForAllTys univ_bndrs $ mkForAllTys ex_bndrs $
rep_ty = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $
mkFunTys rep_arg_tys $
mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
mkTyConApp rep_tycon (mkTyVarTys (map binderVar univ_tvs))
-- See Note [Promoted data constructors] in TyCon
prom_binders = filterEqSpec eq_spec univ_bndrs ++
ex_bndrs ++
prom_binders = map mkNamedBinder (filterEqSpec eq_spec univ_tvs) ++
map mkNamedBinder ex_tvs ++
map mkAnonBinder theta ++
map mkAnonBinder orig_arg_tys
prom_res_kind = orig_res_ty
promoted
= mkPromotedDataCon con name prom_info prom_binders prom_res_kind roles rep_info
promoted = mkPromotedDataCon con name prom_info prom_binders
prom_res_kind roles rep_info
roles = map (const Nominal) (univ_tvs ++ ex_tvs) ++
map (const Representational) orig_arg_tys
......@@ -866,24 +842,24 @@ dataConIsInfix = dcInfix
-- | The universally-quantified type variables of the constructor
dataConUnivTyVars :: DataCon -> [TyVar]
dataConUnivTyVars = dcUnivTyVars
dataConUnivTyVars (MkData { dcUnivTyVars = tvbs }) = map binderVar tvbs
-- | 'TyBinder's for the universally-quantified type variables
dataConUnivTyBinders :: DataCon -> [TyBinder]
dataConUnivTyBinders = dcUnivTyBinders
dataConUnivTyVarBinders :: DataCon -> [TyVarBinder]
dataConUnivTyVarBinders = dcUnivTyVars
-- | The existentially-quantified type variables of the constructor
dataConExTyVars :: DataCon -> [TyVar]
dataConExTyVars = dcExTyVars
dataConExTyVars (MkData { dcExTyVars = tvbs }) = map binderVar tvbs
-- | 'TyBinder's for the existentially-quantified type variables
dataConExTyBinders :: DataCon -> [TyBinder]
dataConExTyBinders = dcExTyBinders
dataConExTyVarBinders :: DataCon -> [TyVarBinder]
dataConExTyVarBinders = dcExTyVars
-- | Both the universal and existentiatial type variables of the constructor
dataConAllTyVars :: DataCon -> [TyVar]
dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
= univ_tvs ++ ex_tvs
= map binderVar (univ_tvs ++ ex_tvs)
-- | Equalities derived from the result type of the data constructor, as written
-- by the programmer in any GADT declaration. This includes *all* GADT-like
......@@ -1020,9 +996,8 @@ dataConBoxer _ = Nothing
--
-- 4) The /original/ result type of the 'DataCon'
dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
dataConSig con@(MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs ++ ex_tvs, dataConTheta con, arg_tys, res_ty)
dataConSig con@(MkData {dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (dataConAllTyVars con, dataConTheta con, arg_tys, res_ty)
dataConInstSig
:: DataCon
......@@ -1035,12 +1010,13 @@ dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
, dcEqSpec = eq_spec, dcOtherTheta = theta
, dcOrigArgTys = arg_tys })
univ_tys
= (ex_tvs'
= ( ex_tvs'
, substTheta subst (eqSpecPreds eq_spec ++ theta)
, substTys subst arg_tys)
where
univ_subst = zipTvSubst univ_tvs univ_tys
(subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst ex_tvs
univ_subst = zipTvSubst (map binderVar univ_tvs) univ_tys
(subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst $
map binderVar ex_tvs
-- | The \"full signature\" of the 'DataCon' returns, in order:
......@@ -1062,7 +1038,7 @@ dataConFullSig :: DataCon
dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
dcEqSpec = eq_spec, dcOtherTheta = theta,
dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
= (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
= (map binderVar univ_tvs, map binderVar ex_tvs, eq_spec, theta, arg_tys, res_ty)
dataConOrigResTy :: DataCon -> Type
dataConOrigResTy dc = dcOrigResTy dc
......@@ -1085,12 +1061,12 @@ dataConUserType :: DataCon -> Type
--
-- NB: If the constructor is part of a data instance, the result type
-- mentions the family tycon, not the internal one.
dataConUserType (MkData { dcUnivTyBinders = univ_bndrs,
dcExTyBinders = ex_bndrs, dcEqSpec = eq_spec,
dataConUserType (MkData { dcUnivTyVars = univ_tvs,
dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
dcOtherTheta = theta, dcOrigArgTys = arg_tys,
dcOrigResTy = res_ty })
= mkForAllTys (filterEqSpec eq_spec univ_bndrs) $
mkForAllTys ex_bndrs $
= mkForAllTys (filterEqSpec eq_spec univ_tvs) $
mkForAllTys ex_tvs $
mkFunTys theta $
mkFunTys arg_tys $
res_ty
......@@ -1110,7 +1086,7 @@ dataConInstArgTys dc@(MkData {dcUnivTyVars = univ_tvs,
= ASSERT2( length univ_tvs == length inst_tys
, text "dataConInstArgTys" <+> ppr dc $$ ppr univ_tvs $$ ppr inst_tys)
ASSERT2( null ex_tvs, ppr dc )
map (substTyWith univ_tvs inst_tys) (dataConRepArgTys dc)
map (substTyWith (map binderVar univ_tvs) inst_tys) (dataConRepArgTys dc)
-- | Returns just the instantiated /value/ argument types of a 'DataCon',
-- (excluding dictionary args)
......@@ -1128,7 +1104,7 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
, text "dataConInstOrigArgTys" <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
map (substTyWith tyvars inst_tys) arg_tys
where
tyvars = univ_tvs ++ ex_tvs
tyvars = map binderVar (univ_tvs ++ ex_tvs)
-- | Returns the argument types of the wrapper, excluding all dictionary arguments
-- and without substituting for any type variables
......
......@@ -6,18 +6,18 @@ import FieldLabel ( FieldLabel )
import Unique ( Uniquable )
import Outputable ( Outputable, OutputableBndr )
import BasicTypes (Arity)
import {-# SOURCE #-} TyCoRep (Type, ThetaType, TyBinder)
import {-# SOURCE #-} TyCoRep (Type, ThetaType, TyVarBinder)
data DataCon
data DataConRep
data EqSpec
filterEqSpec :: [EqSpec] -> [TyBinder] -> [TyBinder]
filterEqSpec :: [EqSpec] -> [TyVarBinder] -> [TyVarBinder]
dataConName :: DataCon -> Name
dataConTyCon :: DataCon -> TyCon
dataConUnivTyBinders :: DataCon -> [TyBinder]
dataConUnivTyVarBinders :: DataCon -> [TyVarBinder]
dataConExTyVars :: DataCon -> [TyVar]
dataConExTyBinders :: DataCon -> [TyBinder]
dataConExTyVarBinders :: DataCon -> [TyVarBinder]
dataConSourceArity :: DataCon -> Arity
dataConFieldLabels :: DataCon -> [FieldLabel]
dataConInstOrigArgTys :: DataCon -> [Type] -> [Type]
......
......@@ -274,13 +274,13 @@ mkDictSelId name clas
sel_names = map idName (classAllSelIds clas)
new_tycon = isNewTyCon tycon
[data_con] = tyConDataCons tycon
binders = dataConUnivTyBinders data_con
tyvars = dataConUnivTyVars data_con
tyvars = dataConUnivTyVarBinders data_con
n_ty_args = length tyvars
arg_tys = dataConRepArgTys data_con -- Includes the dictionary superclasses
val_index = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
sel_ty = mkForAllTys binders $
mkFunTy (mkClassPred clas (mkTyVarTys tyvars)) $
sel_ty = mkForAllTys tyvars $
mkFunTy (mkClassPred clas (mkTyVarTys (map binderVar tyvars))) $
getNth arg_tys val_index
base_info = noCafIdInfo
......@@ -299,8 +299,6 @@ mkDictSelId name clas
-- so that the rule is always available to fire.
-- See Note [ClassOp/DFun selection] in TcInstDcls
n_ty_args = length tyvars
-- This is the built-in rule that goes
-- op (dfT d1 d2) ---> opT d1 d2
rule = BuiltinRule { ru_name = fsLit "Class op " `appendFS`
......@@ -971,10 +969,9 @@ mkFCallId dflags uniq fcall ty
`setArityInfo` arity
`setStrictnessInfo` strict_sig
(bndrs, _) = tcSplitPiTys ty
arity = count isIdLikeBinder bndrs
strict_sig = mkClosedStrictSig (replicate arity topDmd) topRes
(bndrs, _) = tcSplitPiTys ty
arity = count isAnonTyBinder bndrs
strict_sig = mkClosedStrictSig (replicate arity topDmd) topRes
-- the call does not claim to be strict in its arguments, since they
-- may be lifted (foreign import prim) and the called code doesn't
-- necessarily force them. See Trac #11076.
......
......@@ -15,7 +15,7 @@ module PatSyn (
patSynName, patSynArity, patSynIsInfix,
patSynArgs,
patSynMatcher, patSynBuilder,
patSynUnivTyBinders, patSynExTyVars, patSynExTyBinders, patSynSig,
patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders, patSynSig,
patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
patSynFieldType,
......@@ -63,15 +63,13 @@ data PatSyn
-- psArgs
-- Universially-quantified type variables
psUnivTyVars :: [TyVar], -- Two linked fields; see DataCon
psUnivTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
psUnivTyVars :: [TyVarBinder],
-- Required dictionaries (may mention psUnivTyVars)
psReqTheta :: ThetaType,
-- Existentially-quantified type vars
psExTyVars :: [TyVar], -- Two linked fields; see DataCon
psExTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
psExTyVars :: [TyVarBinder],
-- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
psProvTheta :: ThetaType,
......@@ -300,11 +298,9 @@ instance Data.Data PatSyn where
-- | Build a new pattern synonym
mkPatSyn :: Name
-> Bool -- ^ Is the pattern synonym declared infix?
-> ([TyVar], [TyBinder], ThetaType)
-- ^ Universially-quantified type variables
-> ([TyVarBinder], ThetaType) -- ^ Universially-quantified type variables
-- and required dicts
-> ([TyVar], [TyBinder], ThetaType)
-- ^ Existentially-quantified type variables
-> ([TyVarBinder], ThetaType) -- ^ Existentially-quantified type variables
-- and provided dicts
-> [Type] -- ^ Original arguments
-> Type -- ^ Original result type
......@@ -316,14 +312,14 @@ mkPatSyn :: Name
-- NB: The univ and ex vars are both in TyBinder form and TyVar form for
-- convenience. All the TyBinders should be Named!
mkPatSyn name declared_infix
(univ_tvs, univ_bndrs, req_theta)
(ex_tvs, ex_bndrs, prov_theta)
(univ_tvs, req_theta)
(ex_tvs, prov_theta)
orig_args
orig_res_ty
matcher builder field_labels
= MkPatSyn {psName = name, psUnique = getUnique name,
psUnivTyVars = univ_tvs, psUnivTyBinders = univ_bndrs,
psExTyVars = ex_tvs, psExTyBinders = ex_bndrs,
psUnivTyVars = univ_tvs,
psExTyVars = ex_tvs,
psProvTheta = prov_theta, psReqTheta = req_theta,
psInfix = declared_infix,
psArgs = orig_args,
......@@ -359,20 +355,20 @@ patSynFieldType ps label
Just (_, ty) -> ty
Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label)
patSynUnivTyBinders :: PatSyn -> [TyBinder]
patSynUnivTyBinders = psUnivTyBinders
patSynUnivTyVarBinders :: PatSyn -> [TyVarBinder]
patSynUnivTyVarBinders = psUnivTyVars
patSynExTyVars :: PatSyn -> [TyVar]
patSynExTyVars = psExTyVars
patSynExTyVars ps = map binderVar (psExTyVars ps)
patSynExTyBinders :: PatSyn -> [TyBinder]
patSynExTyBinders = psExTyBinders
patSynExTyVarBinders :: PatSyn -> [TyVarBinder]
patSynExTyVarBinders = psExTyVars
patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
, psProvTheta = prov, psReqTheta = req
, psArgs = arg_tys, psOrigResTy = res_ty })
= (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty)
= (map binderVar univ_tvs, req, map binderVar ex_tvs, prov, arg_tys, res_ty)
patSynMatcher :: PatSyn -> (Id,Bool)
patSynMatcher = psMatcher
......@@ -401,7 +397,7 @@ patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
, text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys )
map (substTyWith tyvars inst_tys) arg_tys
where
tyvars = univ_tvs ++ ex_tvs
tyvars = map binderVar (univ_tvs ++ ex_tvs)
patSynInstResTy :: PatSyn -> [Type] -> Type
-- Return the type of whole pattern
......@@ -414,19 +410,19 @@ patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
inst_tys
= ASSERT2( length univ_tvs == length inst_tys
, text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
substTyWith univ_tvs inst_tys res_ty
substTyWith (map binderVar univ_tvs) inst_tys res_ty
-- | Print the type of a pattern synonym. The foralls are printed explicitly
pprPatSynType :: PatSyn -> SDoc
pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
, psExTyVars = ex_tvs, psProvTheta = prov_theta
, psArgs = orig_args, psOrigResTy = orig_res_ty })
= sep [ pprForAllImplicit univ_tvs
= sep [ pprForAll univ_tvs
, pprThetaArrowTy req_theta
, ppWhen insert_empty_ctxt $ parens empty <+> darrow
, pprType sigma_ty ]
where
sigma_ty = mkForAllTys (mkNamedBinders Specified ex_tvs) $
sigma_ty = mkForAllTys ex_tvs $
mkFunTys prov_theta $
mkFunTys orig_args orig_res_ty
insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)
......@@ -970,15 +970,15 @@ getTyDescription ty
TyVarTy _ -> "*"
AppTy fun _ -> getTyDescription fun
TyConApp tycon _ -> getOccString tycon
ForAllTy (Anon _) res -> '-' : '>' : fun_result res
ForAllTy (Named {}) ty -> getTyDescription ty
FunTy _ res -> '-' : '>' : fun_result res
ForAllTy _ ty -> getTyDescription ty
LitTy n -> getTyLitDescription n
CastTy ty _ -> getTyDescription ty
CoercionTy co -> pprPanic "getTyDescription" (ppr co)
}
where
fun_result (ForAllTy (Anon _) res) = '>' : fun_result res
fun_result other = getTyDescription other
fun_result (FunTy _ res) = '>' : fun_result res
fun_result other = getTyDescription other
getTyLitDescription :: TyLit -> String
getTyLitDescription l =
......
......@@ -106,10 +106,11 @@ typeArity ty
= go initRecTc ty
where
go rec_nts ty
| Just (bndr, ty') <- splitPiTy_maybe ty
= if isIdLikeBinder bndr
then typeOneShot (binderType bndr) : go rec_nts ty'
else go rec_nts ty'
| Just (_, ty') <- splitForAllTy_maybe ty
= go rec_nts ty'
| Just (arg,res) <- splitFunTy_maybe ty
= typeOneShot arg : go rec_nts res
| Just (tc,tys) <- splitTyConApp_maybe ty
, Just (ty', _) <- instNewTyCon_maybe tc tys
......@@ -970,13 +971,15 @@ mkEtaWW orig_n orig_expr in_scope orig_ty
| n == 0
= (getTCvInScope subst, reverse eis)
| Just (bndr,ty') <- splitPiTy_maybe ty
= let ((subst', eta_id'), new_n) = caseBinder bndr
(\tv -> (Type.substTyVarBndr subst tv, n))
(\arg_ty -> (freshEtaVar n subst arg_ty, n-1))
in
-- Avoid free vars of the original expression
go new_n subst' ty' (EtaVar eta_id' : eis)
| Just (tv,ty') <- splitForAllTy_maybe ty
, let (subst', tv') = Type.substTyVarBndr subst tv
-- Avoid free vars of the original expression
= go n subst' ty' (EtaVar tv' : eis)
| Just (arg_ty, res_ty) <- splitFunTy_maybe ty
, let (subst', eta_id') = freshEtaId n subst arg_ty
-- Avoid free vars of the original expression
= go (n-1) subst' res_ty (EtaVar eta_id' : eis)
| Just (co, ty') <- topNormaliseNewType_maybe ty
= -- Given this:
......@@ -1009,7 +1012,7 @@ subst_bind = substBindSC
--------------
freshEtaVar :: Int -> TCvSubst -> Type -> (TCvSubst, Var)
freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id)
-- Make a fresh Id, with specified type (after applying substitution)
-- It should be "fresh" in the sense that it's not in the in-scope set
-- of the TvSubstEnv; and it should itself then be added to the in-scope
......@@ -1017,7 +1020,7 @@ freshEtaVar :: Int -> TCvSubst -> Type -> (TCvSubst, Var)
--
-- The Int is just a reasonable starting point for generating a unique;
-- it does not necessarily have to be unique itself.
freshEtaVar n subst ty
freshEtaId n subst ty
= (subst', eta_id')
where
ty' = Type.substTy subst ty
......
......@@ -352,8 +352,10 @@ orphNamesOfType (TyVarTy _) = emptyNameSet
orphNamesOfType (LitTy {}) = emptyNameSet
orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
`unionNameSet` orphNamesOfTypes tys
orphNamesOfType (ForAllTy bndr res) = unitNameSet funTyConName -- NB! See Trac #8535
`unionNameSet` orphNamesOfType (binderType bndr)
orphNamesOfType (ForAllTy bndr res) = orphNamesOfType (binderType bndr)
`unionNameSet` orphNamesOfType res
orphNamesOfType (FunTy arg res) = unitNameSet funTyConName -- NB! See Trac #8535
`unionNameSet` orphNamesOfType arg
`unionNameSet` orphNamesOfType res
orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
orphNamesOfType (CastTy ty co) = orphNamesOfType ty `unionNameSet` orphNamesOfCo co
......
......@@ -558,9 +558,10 @@ lintRhs rhs
, length args == 5
= flip fix binders0 $ \loopBinders binders -> case binders of
-- imitate @lintCoreExpr (Lam ...)@
var : vars -> addLoc (LambdaBodyOf var) $ lintBinder var $ \var' -> do
body_ty <- loopBinders vars
return $ mkPiType var' body_ty
var : vars -> addLoc (LambdaBodyOf var) $
lintBinder var $ \var' ->
do { body_ty <- loopBinders vars
; return $ mkLamType var' body_ty }
-- imitate @lintCoreExpr (App ...)@
[] -> do
fun_ty <- lintCoreExpr fun
......@@ -703,7 +704,7 @@ lintCoreExpr (Lam var expr)
= addLoc (LambdaBodyOf var) $
lintBinder var $ \ var' ->
do { body_ty <- lintCoreExpr expr
; return $ mkPiType var' body_ty }
; return $ mkLamType var' body_ty }
lintCoreExpr e@(Case scrut var alt_ty alts) =
-- Check the scrutinee
......@@ -1097,12 +1098,12 @@ lintType ty@(TyConApp tc tys)
-- arrows can related *unlifted* kinds, so this has to be separate from
-- a dependent forall.
lintType ty@(ForAllTy (Anon t1) t2)
lintType ty@(FunTy t1 t2)
= do { k1 <- lintType t1
; k2 <- lintType t2
; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
lintType t@(ForAllTy (Named tv _vis) ty)
lintType t@(ForAllTy (TvBndr tv _vis) ty)
= do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
; lintTyBndr tv $ \tv' ->
do { k <- lintType ty
......@@ -1192,11 +1193,11 @@ lint_app doc kfn kas
| Just kfn' <- coreView kfn
= go_app in_scope kfn' ka
go_app _ (ForAllTy (Anon kfa) kfb) (_,ka)
go_app _ (FunTy kfa kfb) (_,ka)
= do { unless (ka `eqType` kfa) (addErrL fail_msg)
; return kfb }
go_app in_scope (ForAllTy (Named kv _vis) kfn) (ta,ka)
go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) (ta,ka)
= do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
; return (substTyWithInScope in_scope [kv] [ta] kfn) }
......@@ -1346,7 +1347,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
do {
; (k3, k4, t1, t2, r) <- lintCoercion co
; in_scope <- getInScope
; let tyl = mkNamedForAllTy tv1 Invisible t1
; let tyl = mkInvForAllTy tv1 t1
subst = mkTvSubst in_scope $
-- We need both the free vars of the `t2` and the
-- free vars of the range of the substitution in
......@@ -1355,7 +1356,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
-- linted and `tv2` has the same unique as `tv1`.
-- See Note [The substitution invariant]
unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
tyr = mkNamedForAllTy tv2 Invisible $
tyr = mkInvForAllTy tv2 $
substTy subst t2
; return (k3, k4, tyl, tyr, r) } }
......
......@@ -103,7 +103,7 @@ exprType (Let bind body)
exprType (Case _ _ ty _) = ty
exprType (Cast _ co) = pSnd (coercionKind co)
exprType (Tick _ e) = exprType e
exprType (Lam binder expr) = mkPiType binder (exprType expr)
exprType (Lam binder expr) = mkLamType binder (exprType expr)
exprType e@(App _ _)
= case collectArgs e of