Commit 2cf3cac6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow foralls in instance decls

This patch finally makes it possible to have explicit
foralls in an instance decl
   instance forall (a :: *). Eq a => Eq [a] where ...

This is useful to allow kind signatures or indeed
explicicit kind for-alls; see Trac #11519

I thought it would be really easy, because an instance
declaration already contains an actual HsSigType, so all
the syntactic baggage is there.  But in fact it turned
out that instance declarations were kind-checked a
little differently, because the body kind of the forall
is 'Constraint' rather than '*'.

So I fixed that.  There a slight kludge
(see Note [Body kind of a HsQualTy], but it's still a
significant improvement.

I also did the usual other round of refactoring,
improved a few error messages, tidied up comments etc.
The only significant aspect of all that was

  * Kill mkNakedSpecSigmaTy, mkNakedPhiTy, mkNakedFunTy
    These function names suggest that they do something
    complicated, but acutally they do nothing. So I
    killed them.

  * Swap the arg order of mkNamedBinder, just so that it is
    convenient to say 'map (mkNamedBinder Invisible) tvs'

  * I had to improve isPredTy, to deal with (illegal)
    types like
       (Eq a => Eq [a]) => blah
    See Note [isPeredTy complications] in Type.hs

Still to come: user manual documentation for the
instance-decl change.
parent 8263d09e
......@@ -53,11 +53,12 @@ module HsTypes (
hsScopedTvs, hsWcScopedTvs, dropWildCards,
hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
splitLHsInstDeclTy,
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy,
splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
splitHsFunType, splitHsAppTys,
mkHsOpTy,
splitHsFunType, splitHsAppsTy,
splitHsAppTys, getAppsTyHead_maybe, hsTyGetAppHead_maybe,
mkHsOpTy, mkHsAppTy, mkHsAppTys,
ignoreParens, hsSigType, hsSigWcType,
hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
......@@ -569,9 +570,6 @@ data HsTyLit
| HsStrTy SourceText FastString
deriving (Data, Typeable)
mkHsOpTy :: LHsType name -> Located name -> LHsType name -> HsType name
mkHsOpTy ty1 op ty2 = HsOpTy ty1 op ty2
newtype HsWildCardInfo name -- See Note [The wildcard story for types]
= AnonWildCard (PostRn name (Located Name))
-- A anonymous wild card ('_'). A fresh Name is generated for
......@@ -737,71 +735,6 @@ instance (Outputable arg, Outputable rec)
ppr (RecCon rec) = text "RecCon:" <+> ppr rec
ppr (InfixCon l r) = text "InfixCon:" <+> ppr [l, r]
type LFieldOcc name = Located (FieldOcc name)
-- | Represents an *occurrence* of an unambiguous field. We store
-- both the 'RdrName' the user originally wrote, and after the
-- renamer, the selector function.
data FieldOcc name = FieldOcc { rdrNameFieldOcc :: Located RdrName
-- ^ See Note [Located RdrNames] in HsExpr
, selectorFieldOcc :: PostRn name name
}
deriving Typeable
deriving instance Eq (PostRn name name) => Eq (FieldOcc name)
deriving instance Ord (PostRn name name) => Ord (FieldOcc name)
deriving instance (Data name, Data (PostRn name name)) => Data (FieldOcc name)
instance Outputable (FieldOcc name) where
ppr = ppr . rdrNameFieldOcc
mkFieldOcc :: Located RdrName -> FieldOcc RdrName
mkFieldOcc rdr = FieldOcc rdr PlaceHolder
-- | Represents an *occurrence* of a field that is potentially
-- ambiguous after the renamer, with the ambiguity resolved by the
-- typechecker. We always store the 'RdrName' that the user
-- originally wrote, and store the selector function after the renamer
-- (for unambiguous occurrences) or the typechecker (for ambiguous
-- occurrences).
--
-- See Note [HsRecField and HsRecUpdField] in HsPat and
-- Note [Disambiguating record fields] in TcExpr.
-- See Note [Located RdrNames] in HsExpr
data AmbiguousFieldOcc name
= Unambiguous (Located RdrName) (PostRn name name)
| Ambiguous (Located RdrName) (PostTc name name)
deriving (Typeable)
deriving instance ( Data name
, Data (PostRn name name)
, Data (PostTc name name))
=> Data (AmbiguousFieldOcc name)
instance Outputable (AmbiguousFieldOcc name) where
ppr = ppr . rdrNameAmbiguousFieldOcc
instance OutputableBndr (AmbiguousFieldOcc name) where
pprInfixOcc = pprInfixOcc . rdrNameAmbiguousFieldOcc
pprPrefixOcc = pprPrefixOcc . rdrNameAmbiguousFieldOcc
mkAmbiguousFieldOcc :: Located RdrName -> AmbiguousFieldOcc RdrName
mkAmbiguousFieldOcc rdr = Unambiguous rdr PlaceHolder
rdrNameAmbiguousFieldOcc :: AmbiguousFieldOcc name -> RdrName
rdrNameAmbiguousFieldOcc (Unambiguous (L _ rdr) _) = rdr
rdrNameAmbiguousFieldOcc (Ambiguous (L _ rdr) _) = rdr
selectorAmbiguousFieldOcc :: AmbiguousFieldOcc Id -> Id
selectorAmbiguousFieldOcc (Unambiguous _ sel) = sel
selectorAmbiguousFieldOcc (Ambiguous _ sel) = sel
unambiguousFieldOcc :: AmbiguousFieldOcc Id -> FieldOcc Id
unambiguousFieldOcc (Unambiguous rdr sel) = FieldOcc rdr sel
unambiguousFieldOcc (Ambiguous rdr sel) = FieldOcc rdr sel
ambiguousFieldOcc :: FieldOcc name -> AmbiguousFieldOcc name
ambiguousFieldOcc (FieldOcc rdr sel) = Unambiguous rdr sel
-- Takes details and result type of a GADT data constructor as created by the
-- parser and rejigs them using information about fixities from the renamer.
-- See Note [Sorting out the result type] in RdrHsSyn
......@@ -925,9 +858,6 @@ hsLTyVarBndrsToTypes :: LHsQTyVars name -> [LHsType name]
hsLTyVarBndrsToTypes (HsQTvs { hsq_explicit = tvbs }) = map hsLTyVarBndrToType tvbs
---------------------
mkAnonWildCardTy :: HsType RdrName
mkAnonWildCardTy = HsWildCardTy (AnonWildCard PlaceHolder)
wildCardName :: HsWildCardInfo Name -> Name
wildCardName (AnonWildCard (L _ n)) = n
......@@ -936,12 +866,118 @@ sameWildCard :: Located (HsWildCardInfo name)
-> Located (HsWildCardInfo name) -> Bool
sameWildCard (L l1 (AnonWildCard _)) (L l2 (AnonWildCard _)) = l1 == l2
ignoreParens :: LHsType name -> LHsType name
ignoreParens (L _ (HsParTy ty)) = ignoreParens ty
ignoreParens (L _ (HsAppsTy [L _ (HsAppPrefix ty)])) = ignoreParens ty
ignoreParens ty = ty
{-
************************************************************************
* *
Building types
* *
************************************************************************
-}
mkAnonWildCardTy :: HsType RdrName
mkAnonWildCardTy = HsWildCardTy (AnonWildCard PlaceHolder)
mkHsOpTy :: LHsType name -> Located name -> LHsType name -> HsType name
mkHsOpTy ty1 op ty2 = HsOpTy ty1 op ty2
mkHsAppTy :: LHsType name -> LHsType name -> LHsType name
mkHsAppTy t1 t2 = addCLoc t1 t2 (HsAppTy t1 t2)
mkHsAppTys :: LHsType name -> [LHsType name] -> LHsType name
mkHsAppTys = foldl mkHsAppTy
{-
************************************************************************
* *
Decomposing HsTypes
* *
************************************************************************
-}
---------------------------------
-- splitHsFunType decomposes a type (t1 -> t2 ... -> tn)
-- Breaks up any parens in the result type:
-- splitHsFunType (a -> (b -> c)) = ([a,b], c)
-- Also deals with (->) t1 t2; that is why it only works on LHsType Name
-- (see Trac #9096)
splitHsFunType :: LHsType Name -> ([LHsType Name], LHsType Name)
splitHsFunType (L _ (HsParTy ty))
= splitHsFunType ty
splitHsFunType (L _ (HsFunTy x y))
| (args, res) <- splitHsFunType y
= (x:args, res)
splitHsFunType orig_ty@(L _ (HsAppTy t1 t2))
= go t1 [t2]
where -- Look for (->) t1 t2, possibly with parenthesisation
go (L _ (HsTyVar (L _ fn))) tys | fn == funTyConName
, [t1,t2] <- tys
, (args, res) <- splitHsFunType t2
= (t1:args, res)
go (L _ (HsAppTy t1 t2)) tys = go t1 (t2:tys)
go (L _ (HsParTy ty)) tys = go ty tys
go _ _ = ([], orig_ty) -- Failure to match
splitHsFunType other = ([], other)
--------------------------------
-- | Retrieves the head of an HsAppsTy, if this can be done unambiguously,
-- without consulting fixities.
getAppsTyHead_maybe :: [LHsAppType name] -> Maybe (LHsType name, [LHsType name])
getAppsTyHead_maybe tys = case splitHsAppsTy tys of
([app1:apps], []) -> -- no symbols, some normal types
Just (mkHsAppTys app1 apps, [])
([app1l:appsl, app1r:appsr], [L loc op]) -> -- one operator
Just (L loc (HsTyVar (L loc op)), [mkHsAppTys app1l appsl, mkHsAppTys app1r appsr])
_ -> -- can't figure it out
Nothing
-- | Splits a [HsAppType name] (the payload of an HsAppsTy) into regions of prefix
-- types (normal types) and infix operators.
-- If @splitHsAppsTy tys = (non_syms, syms)@, then @tys@ starts with the first
-- element of @non_syms@ followed by the first element of @syms@ followed by
-- the next element of @non_syms@, etc. It is guaranteed that the non_syms list
-- has one more element than the syms list.
splitHsAppsTy :: [LHsAppType name] -> ([[LHsType name]], [Located name])
splitHsAppsTy = go [] [] []
where
go acc acc_non acc_sym [] = (reverse (reverse acc : acc_non), reverse acc_sym)
go acc acc_non acc_sym (L _ (HsAppPrefix ty) : rest)
= go (ty : acc) acc_non acc_sym rest
go acc acc_non acc_sym (L _ (HsAppInfix op) : rest)
= go [] (reverse acc : acc_non) (op : acc_sym) rest
-- Retrieve the name of the "head" of a nested type application
-- somewhat like splitHsAppTys, but a little more thorough
-- used to examine the result of a GADT-like datacon, so it doesn't handle
-- *all* cases (like lists, tuples, (~), etc.)
hsTyGetAppHead_maybe :: LHsType name -> Maybe (Located name, [LHsType name])
hsTyGetAppHead_maybe = go []
where
go tys (L _ (HsTyVar ln)) = Just (ln, tys)
go tys (L _ (HsAppsTy apps))
| Just (head, args) <- getAppsTyHead_maybe apps
= go (args ++ tys) head
go tys (L _ (HsAppTy l r)) = go (r : tys) l
go tys (L _ (HsOpTy l (L loc n) r)) = Just (L loc n, l : r : tys)
go tys (L _ (HsParTy t)) = go tys t
go tys (L _ (HsKindSig t _)) = go tys t
go _ _ = Nothing
splitHsAppTys :: LHsType Name -> [LHsType Name] -> (LHsType Name, [LHsType Name])
-- no need to worry about HsAppsTy here
splitHsAppTys (L _ (HsAppTy f a)) as = splitHsAppTys f (a:as)
splitHsAppTys (L _ (HsParTy f)) as = splitHsAppTys f as
splitHsAppTys f as = (f,as)
--------------------------------
splitLHsPatSynTy :: LHsType name
-> ( [LHsTyVarBndr name]
, LHsContext name -- Required
......@@ -974,48 +1010,101 @@ splitLHsQualTy :: LHsType name -> (LHsContext name, LHsType name)
splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt, body)
splitLHsQualTy body = (noLoc [], body)
splitLHsInstDeclTy
:: LHsSigType Name
splitLHsInstDeclTy :: LHsSigType Name
-> ([Name], LHsContext Name, LHsType Name)
-- Split up an instance decl type, returning the pieces
-- Split up an instance decl type, returning the pieces
splitLHsInstDeclTy (HsIB { hsib_vars = itkvs
, hsib_body = inst_ty })
= (itkvs, cxt, body_ty)
| (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty
= (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
-- Return implicitly bound type and kind vars
-- For an instance decl, all of them are in scope
where
(cxt, body_ty) = splitLHsQualTy inst_ty
-- splitHsFunType decomposes a type (t1 -> t2 ... -> tn)
-- Breaks up any parens in the result type:
-- splitHsFunType (a -> (b -> c)) = ([a,b], c)
-- Also deals with (->) t1 t2; that is why it only works on LHsType Name
-- (see Trac #9096)
splitHsFunType :: LHsType Name -> ([LHsType Name], LHsType Name)
splitHsFunType (L _ (HsParTy ty))
= splitHsFunType ty
getLHsInstDeclHead :: LHsSigType name -> LHsType name
getLHsInstDeclHead inst_ty
| (_tvs, _cxt, body_ty) <- splitLHsSigmaTy (hsSigType inst_ty)
= body_ty
splitHsFunType (L _ (HsFunTy x y))
| (args, res) <- splitHsFunType y
= (x:args, res)
getLHsInstDeclClass_maybe :: LHsSigType name -> Maybe (Located name)
-- Works on (HsSigType RdrName)
getLHsInstDeclClass_maybe inst_ty
= do { let head_ty = getLHsInstDeclHead inst_ty
; (cls, _) <- hsTyGetAppHead_maybe head_ty
; return cls }
splitHsFunType orig_ty@(L _ (HsAppTy t1 t2))
= go t1 [t2]
where -- Look for (->) t1 t2, possibly with parenthesisation
go (L _ (HsTyVar (L _ fn))) tys | fn == funTyConName
, [t1,t2] <- tys
, (args, res) <- splitHsFunType t2
= (t1:args, res)
go (L _ (HsAppTy t1 t2)) tys = go t1 (t2:tys)
go (L _ (HsParTy ty)) tys = go ty tys
go _ _ = ([], orig_ty) -- Failure to match
{-
************************************************************************
* *
FieldOcc
* *
************************************************************************
-}
splitHsFunType other = ([], other)
type LFieldOcc name = Located (FieldOcc name)
ignoreParens :: LHsType name -> LHsType name
ignoreParens (L _ (HsParTy ty)) = ignoreParens ty
ignoreParens (L _ (HsAppsTy [L _ (HsAppPrefix ty)])) = ignoreParens ty
ignoreParens ty = ty
-- | Represents an *occurrence* of an unambiguous field. We store
-- both the 'RdrName' the user originally wrote, and after the
-- renamer, the selector function.
data FieldOcc name = FieldOcc { rdrNameFieldOcc :: Located RdrName
-- ^ See Note [Located RdrNames] in HsExpr
, selectorFieldOcc :: PostRn name name
}
deriving Typeable
deriving instance Eq (PostRn name name) => Eq (FieldOcc name)
deriving instance Ord (PostRn name name) => Ord (FieldOcc name)
deriving instance (Data name, Data (PostRn name name)) => Data (FieldOcc name)
instance Outputable (FieldOcc name) where
ppr = ppr . rdrNameFieldOcc
mkFieldOcc :: Located RdrName -> FieldOcc RdrName
mkFieldOcc rdr = FieldOcc rdr PlaceHolder
-- | Represents an *occurrence* of a field that is potentially
-- ambiguous after the renamer, with the ambiguity resolved by the
-- typechecker. We always store the 'RdrName' that the user
-- originally wrote, and store the selector function after the renamer
-- (for unambiguous occurrences) or the typechecker (for ambiguous
-- occurrences).
--
-- See Note [HsRecField and HsRecUpdField] in HsPat and
-- Note [Disambiguating record fields] in TcExpr.
-- See Note [Located RdrNames] in HsExpr
data AmbiguousFieldOcc name
= Unambiguous (Located RdrName) (PostRn name name)
| Ambiguous (Located RdrName) (PostTc name name)
deriving (Typeable)
deriving instance ( Data name
, Data (PostRn name name)
, Data (PostTc name name))
=> Data (AmbiguousFieldOcc name)
instance Outputable (AmbiguousFieldOcc name) where
ppr = ppr . rdrNameAmbiguousFieldOcc
instance OutputableBndr (AmbiguousFieldOcc name) where
pprInfixOcc = pprInfixOcc . rdrNameAmbiguousFieldOcc
pprPrefixOcc = pprPrefixOcc . rdrNameAmbiguousFieldOcc
mkAmbiguousFieldOcc :: Located RdrName -> AmbiguousFieldOcc RdrName
mkAmbiguousFieldOcc rdr = Unambiguous rdr PlaceHolder
rdrNameAmbiguousFieldOcc :: AmbiguousFieldOcc name -> RdrName
rdrNameAmbiguousFieldOcc (Unambiguous (L _ rdr) _) = rdr
rdrNameAmbiguousFieldOcc (Ambiguous (L _ rdr) _) = rdr
selectorAmbiguousFieldOcc :: AmbiguousFieldOcc Id -> Id
selectorAmbiguousFieldOcc (Unambiguous _ sel) = sel
selectorAmbiguousFieldOcc (Ambiguous _ sel) = sel
unambiguousFieldOcc :: AmbiguousFieldOcc Id -> FieldOcc Id
unambiguousFieldOcc (Unambiguous rdr sel) = FieldOcc rdr sel
unambiguousFieldOcc (Ambiguous rdr sel) = FieldOcc rdr sel
ambiguousFieldOcc :: FieldOcc name -> AmbiguousFieldOcc name
ambiguousFieldOcc (FieldOcc rdr sel) = Unambiguous rdr sel
{-
************************************************************************
......
......@@ -56,8 +56,6 @@ module HsUtils(
mkHsAppTy, mkHsAppTys, userHsTyVarBndrs, userHsLTyVarBndrs,
mkLHsSigType, mkLHsSigWcType, mkClassOpSigs,
nlHsAppTy, nlHsTyVar, nlHsFunTy, nlHsTyConApp,
getAppsTyHead_maybe, hsTyGetAppHead_maybe, splitHsAppsTy,
getLHsInstDeclClass_maybe,
-- Stmts
mkTransformStmt, mkTransformByStmt, mkBodyStmt, mkBindStmt, mkTcBindStmt,
......@@ -168,12 +166,6 @@ mkMatchGroupName origin matches = MG { mg_alts = mkLocatedList matches
, mg_res_ty = placeHolderType
, mg_origin = origin }
mkHsAppTy :: LHsType name -> LHsType name -> LHsType name
mkHsAppTy t1 t2 = addCLoc t1 t2 (HsAppTy t1 t2)
mkHsAppTys :: LHsType name -> [LHsType name] -> LHsType name
mkHsAppTys = foldl mkHsAppTy
mkHsApp :: LHsExpr name -> LHsExpr name -> LHsExpr name
mkHsApp e1 e2 = addCLoc e1 e2 (HsApp e1 e2)
......@@ -1141,60 +1133,3 @@ lPatImplicits = hs_lpat
pat_explicit = maybe True (i<) (rec_dotdot fs)]
details (InfixCon p1 p2) = hs_lpat p1 `unionNameSet` hs_lpat p2
{-
************************************************************************
* *
Dealing with HsAppsTy
* *
************************************************************************
-}
-- | Retrieves the head of an HsAppsTy, if this can be done unambiguously,
-- without consulting fixities.
getAppsTyHead_maybe :: [LHsAppType name] -> Maybe (LHsType name, [LHsType name])
getAppsTyHead_maybe tys = case splitHsAppsTy tys of
([app1:apps], []) -> -- no symbols, some normal types
Just (mkHsAppTys app1 apps, [])
([app1l:appsl, app1r:appsr], [L loc op]) -> -- one operator
Just (L loc (HsTyVar (L loc op)), [mkHsAppTys app1l appsl, mkHsAppTys app1r appsr])
_ -> -- can't figure it out
Nothing
-- | Splits a [HsAppType name] (the payload of an HsAppsTy) into regions of prefix
-- types (normal types) and infix operators.
-- If @splitHsAppsTy tys = (non_syms, syms)@, then @tys@ starts with the first
-- element of @non_syms@ followed by the first element of @syms@ followed by
-- the next element of @non_syms@, etc. It is guaranteed that the non_syms list
-- has one more element than the syms list.
splitHsAppsTy :: [LHsAppType name] -> ([[LHsType name]], [Located name])
splitHsAppsTy = go [] [] []
where
go acc acc_non acc_sym [] = (reverse (reverse acc : acc_non), reverse acc_sym)
go acc acc_non acc_sym (L _ (HsAppPrefix ty) : rest)
= go (ty : acc) acc_non acc_sym rest
go acc acc_non acc_sym (L _ (HsAppInfix op) : rest)
= go [] (reverse acc : acc_non) (op : acc_sym) rest
-- retrieve the name of the "head" of a nested type application
-- somewhat like splitHsAppTys, but a little more thorough
-- used to examine the result of a GADT-like datacon, so it doesn't handle
-- *all* cases (like lists, tuples, (~), etc.)
hsTyGetAppHead_maybe :: LHsType name -> Maybe (Located name, [LHsType name])
hsTyGetAppHead_maybe = go []
where
go tys (L _ (HsTyVar ln)) = Just (ln, tys)
go tys (L _ (HsAppsTy apps))
| Just (head, args) <- getAppsTyHead_maybe apps
= go (args ++ tys) head
go tys (L _ (HsAppTy l r)) = go (r : tys) l
go tys (L _ (HsOpTy l (L loc n) r)) = Just (L loc n, l : r : tys)
go tys (L _ (HsParTy t)) = go tys t
go tys (L _ (HsKindSig t _)) = go tys t
go _ _ = Nothing
getLHsInstDeclClass_maybe :: LHsSigType name -> Maybe (Located name)
-- Works on (HsSigType RdrName)
getLHsInstDeclClass_maybe inst_ty
= do { let (_, tau) = splitLHsQualTy (hsSigType inst_ty)
; (cls, _) <- hsTyGetAppHead_maybe tau
; return cls }
......@@ -633,8 +633,7 @@ checkCanonicalInstances cls poly_ty mbinds = do
-- stolen from TcInstDcls
instDeclCtxt1 :: LHsSigType Name -> SDoc
instDeclCtxt1 hs_inst_ty
| (_, _, head_ty) <- splitLHsInstDeclTy hs_inst_ty
= inst_decl_ctxt (ppr head_ty)
= inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
inst_decl_ctxt :: SDoc -> SDoc
inst_decl_ctxt doc = hang (text "in the instance declaration for")
......
......@@ -833,7 +833,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
= do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
-- Include kind variables! Trac #7916
my_theta = pickQuantifiablePreds free_tvs inferred_theta
binders = [ mkNamedBinder tv Invisible
binders = [ mkNamedBinder Invisible tv
| tv <- qtvs
, tv `elemVarSet` free_tvs ]
; return (binders, my_theta) }
......@@ -892,7 +892,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
spec_tv_set = mkVarSet $ map snd annotated_tvs
mk_binders free_tvs
= [ mkNamedBinder tv vis
= [ mkNamedBinder vis tv
| tv <- qtvs
, tv `elemVarSet` free_tvs
, let vis | tv `elemVarSet` spec_tv_set = Specified
......
......@@ -232,28 +232,13 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
-> LHsSigType Name
-> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigType, but for a class instance declaration
-- The significant difference is that we expect a /constraint/
-- not a /type/ for the bit after the '=>'.
tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars
, hsib_body = hs_qual_ty })
-- An explicit forall in an instance declaration isn't
-- allowed, so there won't be any HsForAllTy here
= setSrcSpan (getLoc hs_qual_ty) $
do { (tkvs, phi_ty) <- solveEqualities $
tcImplicitTKBndrsType sig_vars $
do { theta <- tcHsContext cxt
; head_ty' <- tc_lhs_type typeLevelMode
head_ty constraintKind
; return (mkPhiTy theta head_ty') }
; let inst_ty = mkSpecForAllTys tkvs phi_ty
tcHsClsInstType user_ctxt hs_inst_ty
= setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
do { inst_ty <- tc_hs_sig_type hs_inst_ty constraintKind
; inst_ty <- kindGeneralizeType inst_ty
; inst_ty <- zonkTcType inst_ty
; checkValidInstance user_ctxt hs_inst_ty inst_ty }
where
(cxt, head_ty) = splitLHsQualTy hs_qual_ty
-- Used for 'VECTORISE [SCALAR] instance' declarations
--
tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type])
tcHsVectInst ty
| Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
......@@ -478,7 +463,7 @@ tc_fun_type mode ty1 ty2 exp_kind
; res_lev <- newFlexiTyVarTy levityTy
; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev)
; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev)
; checkExpectedKind (mkNakedFunTy ty1' ty2') liftedTypeKind exp_kind }
; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
------------------------------------------
-- See also Note [Bidirectional type checking]
......@@ -508,34 +493,32 @@ tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
= tc_fun_type mode ty1 ty2 exp_kind
--------- Foralls
tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
-- Do not kind-generalise here. See Note [Kind generalisation]
| isConstraintKind exp_kind
= failWithTc (hang (text "Illegal constraint:") 2 (ppr hs_ty))
| otherwise
tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
= fmap fst $
tcExplicitTKBndrs hs_tvs $ \ tvs' ->
-- Do not kind-generalise here! See Note [Kind generalisation]
-- Why exp_kind? See Note [Body kind of forall]
-- Why exp_kind? See Note [Body kind of HsForAllTy]
do { ty' <- tc_lhs_type mode ty exp_kind
; let bound_vars = allBoundVariables ty'
; return (mkNakedSpecSigmaTy tvs' [] ty', bound_vars) }
bndrs = map (mkNamedBinder Specified) tvs'
; return (mkForAllTys bndrs ty', bound_vars) }
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
| null (unLoc ctxt)
= tc_lhs_type mode ty exp_kind
| otherwise
= do { ctxt' <- tc_hs_context mode ctxt
; ty' <- if null (unLoc ctxt) then -- Plain forall, no context
tc_lhs_type mode ty exp_kind
-- Why exp_kind? See Note [Body kind of forall]
else
-- If there is a context, then this forall is really a
-- _function_, so the kind of the result really is *
-- The body kind (result of the function) can be * or #, hence ekOpen
do { ek <- ekOpen
-- See Note [Body kind of a HsQualTy]
; ty' <- if isConstraintKind exp_kind
then tc_lhs_type mode ty constraintKind
else do { ek <- ekOpen -- The body kind (result of the
-- function) can be * or #, hence ekOpen
; ty <- tc_lhs_type mode ty ek
; checkExpectedKind ty liftedTypeKind exp_kind }
; return (mkNakedPhiTy ctxt' ty') }
; return (mkPhiTy ctxt' ty') }
--------- Lists, arrays, and tuples
tc_hs_type mode (HsListTy elt_ty) exp_kind
......@@ -1101,8 +1084,8 @@ look at the TyCon or Class involved.
This is horribly delicate. I hate it. A good example of how
delicate it is can be seen in Trac #7903.
Note [Body kind of a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The body of a forall is usually a type, but in principle
there's no reason to prohibit *unlifted* types.
In fact, GHC can itself construct a function with an
......@@ -1112,37 +1095,6 @@ typecheck/should_compile/tc170).
Moreover in instance heads we get forall-types with
kind Constraint.
Moreover if we have a signature
f :: Int#
then we represent it as (HsForAll Implicit [] [] Int#). And this must
be legal! We can't drop the empty forall until *after* typechecking
the body because of kind polymorphism:
Typeable :: forall k. k -> Constraint
data Apply f t = Apply (f t)
-- Apply :: forall k. (k -> *) -> k -> *
instance Typeable Apply where ...
Then the dfun has type
df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)
f :: Typeable Apply
f :: forall (t:k->*) (a:k). t a -> t a