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

Allow kind-variable binders in type signatures

This is the last major addition to the kind-polymorphism story,
by allowing (Trac #5938)

 type family F a   -- F :: forall k. k -> *
 data T a          -- T :: forall k. k -> *
 type instance F (T (a :: Maybe k)) = Char

The new thing is the explicit 'k' in the type signature on 'a',
which itself is inside a type pattern for F.

Main changes are:

* HsTypes.HsBSig now has a *pair* (kvs, tvs) of binders,
  the kind variables and the type variables

* extractHsTyRdrTyVars returns a pair (kvs, tvs)
  and the function itself has moved from RdrHsSyn to RnTypes

* Quite a bit of fiddling with
     TcHsType.tcHsPatSigType and tcPatSig
  which have become a bit simpler.  I'm still not satisfied
  though.  There's some consequential fiddling in TcRules too.

* Removed the unused HsUtils.collectSigTysFromPats

There's a consequential wibble to Haddock too
parent 3f46b1e3
......@@ -352,8 +352,12 @@ repInstD (L loc (ClsInstD ty binds prags ats))
Just (tvs, cxt, cls, tys) = splitHsInstDeclTy_maybe (unLoc ty)
repFamInstD :: FamInstDecl Name -> DsM (Core TH.DecQ)
repFamInstD (FamInstDecl { fid_tycon = tc_name, fid_pats = HsBSig tys tv_names, fid_defn = defn })
= do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences]
repFamInstD (FamInstDecl { fid_tycon = tc_name
, fid_pats = HsBSig tys (kv_names, tv_names)
, fid_defn = defn })
= WARN( not (null kv_names), ppr kv_names ) -- We have not yet dealt with kind
-- polymorphism in Template Haskell (sigh)
do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences]
; let loc = getLoc tc_name
hs_tvs = [ L loc (UserTyVar n) | n <- tv_names] -- Yuk
; addTyClTyVarBinds hs_tvs $ \ bndrs ->
......
......@@ -125,9 +125,15 @@ type LHsTyVarBndr name = Located (HsTyVarBndr name)
data HsBndrSig sig
= HsBSig
sig
[Name] -- The *binding* type/kind names of this signature
sig -- The signature; typically a type
([Name], [Name]) -- The *binding* (kind, type) names of
-- this signature
-- See Note [HsBSig binder lists]
deriving (Data, Typeable)
-- Note [HsBSig binder lists]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Consider a binder (or pattern) decoarated with a type or kind,
-- \ (x :: a -> a). blah
-- forall (a :: k -> *) (b :: k). blah
......@@ -135,6 +141,7 @@ data HsBndrSig sig
-- renamer can decorate it with the variables bound
-- by the pattern ('a' in the first example, 'k' in the second),
-- assuming that neither of them is in scope already
-- See also Note [Kind and type-variable binders] in RnTypes
placeHolderBndrs :: [Name]
-- Used for the NameSet in FunBind and PatBind prior to the renamer
......
......@@ -66,7 +66,6 @@ module HsUtils(
collectPatBinders, collectPatsBinders,
collectLStmtsBinders, collectStmtsBinders,
collectLStmtBinders, collectStmtBinders,
collectSigTysFromPats, collectSigTysFromPat,
hsLTyClDeclBinders, hsTyClDeclBinders, hsTyClDeclsBinders,
hsForeignDeclsBinders, hsGroupBinders, hsFamInstBinders,
......@@ -266,7 +265,7 @@ mkHsString :: String -> HsLit
mkHsString s = HsString (mkFastString s)
mkHsBSig :: a -> HsBndrSig a
mkHsBSig x = HsBSig x placeHolderBndrs
mkHsBSig x = HsBSig x (placeHolderBndrs, placeHolderBndrs)
-------------
userHsTyVarBndrs :: SrcSpan -> [name] -> [Located (HsTyVarBndr name)]
......@@ -769,34 +768,3 @@ lPatImplicits = hs_lpat
pat_explicit = maybe True (i<) (rec_dotdot fs)]
details (InfixCon p1 p2) = hs_lpat p1 `unionNameSets` hs_lpat p2
\end{code}
%************************************************************************
%* *
Collecting type signatures from patterns
%* *
%************************************************************************
\begin{code}
collectSigTysFromPats :: [InPat name] -> [HsBndrSig (LHsType name)]
collectSigTysFromPats pats = foldr collect_sig_lpat [] pats
collectSigTysFromPat :: InPat name -> [HsBndrSig (LHsType name)]
collectSigTysFromPat pat = collect_sig_lpat pat []
collect_sig_lpat :: InPat name -> [HsBndrSig (LHsType name)] -> [HsBndrSig (LHsType name)]
collect_sig_lpat pat acc = collect_sig_pat (unLoc pat) acc
collect_sig_pat :: Pat name -> [HsBndrSig (LHsType name)] -> [HsBndrSig (LHsType name)]
collect_sig_pat (SigPatIn pat ty) acc = collect_sig_lpat pat (ty:acc)
collect_sig_pat (LazyPat pat) acc = collect_sig_lpat pat acc
collect_sig_pat (BangPat pat) acc = collect_sig_lpat pat acc
collect_sig_pat (AsPat _ pat) acc = collect_sig_lpat pat acc
collect_sig_pat (ParPat pat) acc = collect_sig_lpat pat acc
collect_sig_pat (ListPat pats _) acc = foldr collect_sig_lpat acc pats
collect_sig_pat (PArrPat pats _) acc = foldr collect_sig_lpat acc pats
collect_sig_pat (TuplePat pats _ _) acc = foldr collect_sig_lpat acc pats
collect_sig_pat (ConPatIn _ ps) acc = foldr collect_sig_lpat acc (hsConPatArgs ps)
collect_sig_pat _ acc = acc -- Literals, vars, wildcard
\end{code}
......@@ -729,7 +729,7 @@ data_or_newtype :: { Located NewOrData }
opt_kind_sig :: { Located (Maybe (HsBndrSig (LHsKind RdrName))) }
: { noLoc Nothing }
| '::' kind { LL (Just (HsBSig $2 placeHolderBndrs)) }
| '::' kind { LL (Just (mkHsBSig $2)) }
-- tycl_hdr parses the header of a class or data type decl,
-- which takes the form
......@@ -876,7 +876,7 @@ rule_var_list :: { [RuleBndr RdrName] }
rule_var :: { RuleBndr RdrName }
: varid { RuleBndr $1 }
| '(' varid '::' ctype ')' { RuleBndrSig $2 (HsBSig $4 placeHolderBndrs) }
| '(' varid '::' ctype ')' { RuleBndrSig $2 (mkHsBSig $4) }
-----------------------------------------------------------------------------
-- Warnings and deprecations (c.f. rules)
......@@ -1109,7 +1109,7 @@ tv_bndrs :: { [LHsTyVarBndr RdrName] }
tv_bndr :: { LHsTyVarBndr RdrName }
: tyvar { L1 (UserTyVar (unLoc $1)) }
| '(' tyvar '::' kind ')' { LL (KindedTyVar (unLoc $2) (HsBSig $4 placeHolderBndrs)) }
| '(' tyvar '::' kind ')' { LL (KindedTyVar (unLoc $2) (mkHsBSig $4)) }
fds :: { Located [Located (FunDep RdrName)] }
: {- empty -} { noLoc [] }
......
......@@ -377,7 +377,7 @@ ifaceArrow ifT1 ifT2 = IfaceFunTy ifT1 ifT2
toHsTvBndr :: IfaceTvBndr -> LHsTyVarBndr RdrName
toHsTvBndr (tv,k) = noLoc $ KindedTyVar (mkRdrUnqual (mkTyVarOccFS tv)) bsig
where
bsig = HsBSig (toHsKind k) placeHolderBndrs
bsig = mkHsBSig (toHsKind k)
ifaceExtRdrName :: Name -> RdrName
ifaceExtRdrName name = mkOrig (nameModule name) (nameOccName name)
......
......@@ -5,8 +5,6 @@ Functions over HsSyn specialised to RdrName.
\begin{code}
module RdrHsSyn (
extractHsTyRdrTyVars, extractHsTysRdrTyVars,
mkHsOpApp,
mkHsIntegral, mkHsFractional, mkHsIsString,
mkHsDo, mkHsSplice, mkTopSpliceDecl,
......@@ -78,77 +76,15 @@ import Bag ( Bag, emptyBag, consBag )
import Outputable
import FastString
import Maybes
import Util ( filterOut )
import Control.Applicative ((<$>))
import Control.Monad
import Text.ParserCombinators.ReadP as ReadP
import Data.List ( nub )
import Data.Char
#include "HsVersions.h"
\end{code}
%************************************************************************
%* *
\subsection{A few functions over HsSyn at RdrName}
%* *
%************************************************************************
extractHsTyRdrNames finds the free variables of a HsType
It's used when making the for-alls explicit.
\begin{code}
extractHsTyRdrTyVars :: LHsType RdrName -> [RdrName]
extractHsTyRdrTyVars ty = nub (extract_lty ty [])
extractHsTysRdrTyVars :: [LHsType RdrName] -> [RdrName]
extractHsTysRdrTyVars ty = nub (extract_ltys ty [])
extract_lctxt :: LHsContext RdrName -> [RdrName] -> [RdrName]
extract_lctxt ctxt acc = foldr extract_lty acc (unLoc ctxt)
extract_ltys :: [LHsType RdrName] -> [RdrName] -> [RdrName]
extract_ltys tys acc = foldr extract_lty acc tys
-- IA0_NOTE: Should this function also return kind variables?
-- (explicit kind poly)
extract_lty :: LHsType RdrName -> [RdrName] -> [RdrName]
extract_lty (L _ ty) acc
= case ty of
HsTyVar tv -> extract_tv tv acc
HsBangTy _ ty -> extract_lty ty acc
HsRecTy flds -> foldr (extract_lty . cd_fld_type) acc flds
HsAppTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsListTy ty -> extract_lty ty acc
HsPArrTy ty -> extract_lty ty acc
HsTupleTy _ tys -> extract_ltys tys acc
HsFunTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsIParamTy _ ty -> extract_lty ty acc
HsEqTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsOpTy ty1 (_, (L _ tv)) ty2 -> extract_tv tv (extract_lty ty1 (extract_lty ty2 acc))
HsParTy ty -> extract_lty ty acc
HsCoreTy {} -> acc -- The type is closed
HsQuasiQuoteTy {} -> acc -- Quasi quotes mention no type variables
HsSpliceTy {} -> acc -- Type splices mention no type variables
HsKindSig ty _ -> extract_lty ty acc
HsForAllTy _ [] cx ty -> extract_lctxt cx (extract_lty ty acc)
HsForAllTy _ tvs cx ty -> acc ++ (filterOut (`elem` locals) $
extract_lctxt cx (extract_lty ty []))
where
locals = hsLTyVarNames tvs
HsDocTy ty _ -> extract_lty ty acc
HsExplicitListTy _ tys -> extract_ltys tys acc
HsExplicitTupleTy _ tys -> extract_ltys tys acc
HsTyLit _ -> acc
HsWrapTy _ _ -> panic "extract_lty"
extract_tv :: RdrName -> [RdrName] -> [RdrName]
extract_tv tv acc | isRdrTyVar tv = tv : acc
| otherwise = acc
\end{code}
%************************************************************************
%* *
\subsection{Construction functions for Rdr stuff}
......
......@@ -24,7 +24,6 @@ import {-# SOURCE #-} TcSplice ( runQuasiQuoteDecl )
import HsSyn
import RdrName
import RdrHsSyn ( extractHsTysRdrTyVars )
import RnTypes
import RnBinds
import RnEnv
......@@ -490,10 +489,13 @@ rnFamInstDecl mb_cls (FamInstDecl { fid_tycon = tycon, fid_pats = HsBSig pats _,
[] -> pprPanic "rnFamInstDecl" (ppr tycon)
(L loc _ : []) -> loc
(L loc _ : ps) -> combineSrcSpans loc (getLoc (last ps))
; tv_names <- mkTyVarBndrNames mb_cls (map (L loc) (extractHsTysRdrTyVars pats))
(kv_rdr_names, tv_rdr_names) = extractHsTysRdrTyVars pats
; kv_names <- mkTyVarBndrNames mb_cls (map (L loc) kv_rdr_names)
; tv_names <- mkTyVarBndrNames mb_cls (map (L loc) tv_rdr_names)
-- All the free vars of the family patterns
-- with a sensible binding location
; bindLocalNamesFV tv_names $
; bindLocalNamesFV kv_names $
bindLocalNamesFV tv_names $
do { (pats', pat_fvs) <- rnLHsTypes (TyDataCtx tycon) pats
; (defn', rhs_fvs) <- rnTyDefn tycon defn
......@@ -505,7 +507,7 @@ rnFamInstDecl mb_cls (FamInstDecl { fid_tycon = tycon, fid_pats = HsBSig pats _,
; unless (null bad_tvs) (badAssocRhs bad_tvs)
; return ( FamInstDecl { fid_tycon = tycon'
, fid_pats = HsBSig pats' tv_names
, fid_pats = HsBSig pats' (kv_names, tv_names)
, fid_defn = defn' }
, (rhs_fvs `plusFV` pat_fvs) `addOneFV` unLoc tycon') } }
-- type instance => use, hence addOneFV
......@@ -1092,7 +1094,7 @@ rnConDecl decl@(ConDecl { con_name = name, con_qvars = tvs
fvs1 `plusFV` fvs2 `plusFV` fvs3) }}
where
doc = ConDeclCtx name
get_rdr_tvs tys = extractHsTysRdrTyVars (cxt ++ tys)
get_rdr_tvs tys = snd (extractHsTysRdrTyVars (cxt ++ tys))
rnConResult :: HsDocContext -> Name
-> HsConDetails (LHsType Name) [ConDeclField Name]
......
......@@ -26,7 +26,9 @@ module RnTypes (
rnSplice, checkTH,
-- Binding related stuff
bindSigTyVarsFV, bindHsTyVars, bindTyVarsRn, rnHsBndrSig
bindSigTyVarsFV, bindHsTyVars, bindTyVarsRn, rnHsBndrSig,
extractHsTyRdrTyVars, extractHsTysRdrTyVars
) where
import {-# SOURCE #-} RnExpr( rnLExpr )
......@@ -36,7 +38,6 @@ import {-# SOURCE #-} TcSplice( runQuasiQuoteType )
import DynFlags
import HsSyn
import RdrHsSyn ( extractHsTyRdrTyVars, extractHsTysRdrTyVars )
import RnHsDoc ( rnLHsDoc, rnMbLHsDoc )
import RnEnv
import TcRnMonad
......@@ -53,6 +54,7 @@ import BasicTypes ( IPName(..), ipNameName, compareFixity, funTyFixity, negateFi
Fixity(..), FixityDirection(..) )
import Outputable
import FastString
import Data.List ( nub )
import Control.Monad ( unless )
#include "HsVersions.h"
......@@ -129,7 +131,11 @@ rnHsTyKi isType doc (HsForAllTy Implicit _ lctxt@(L _ ctxt) ty)
name_env <- getLocalRdrEnv
loc <- getSrcSpanM
let
mentioned = extractHsTysRdrTyVars (ty:ctxt)
(_kvs, mentioned) = extractHsTysRdrTyVars (ty:ctxt)
-- In for-all types we don't bring in scope
-- kind variables mentioned in kind signatures
-- (Well, not yet anyway....)
-- f :: Int -> T (a::k) -- Not allowed
-- Don't quantify over type variables that are in scope;
-- when GlasgowExts is off, there usually won't be any, except for
......@@ -144,7 +150,7 @@ rnHsTyKi isType doc ty@(HsForAllTy Explicit forall_tyvars lctxt@(L _ ctxt) tau)
= ASSERT ( isType ) do { -- Explicit quantification.
-- Check that the forall'd tyvars are actually
-- mentioned in the type, and produce a warning if not
let mentioned = extractHsTysRdrTyVars (tau:ctxt)
let (_kvs, mentioned) = extractHsTysRdrTyVars (tau:ctxt)
in_type_doc = ptext (sLit "In the type") <+> quotes (ppr ty)
; warnUnusedForAlls (in_type_doc $$ docOfHsDocContext doc) forall_tyvars mentioned
......@@ -383,15 +389,17 @@ rnHsBndrSig :: Bool -- True <=> type sig, False <=> kind sig
-> (HsBndrSig (LHsType Name) -> RnM (a, FreeVars))
-> RnM (a, FreeVars)
rnHsBndrSig is_type doc (HsBSig ty@(L loc _) _) thing_inside
= do { name_env <- getLocalRdrEnv
; let tv_bndrs = [ tv | tv <- extractHsTyRdrTyVars ty
, not (tv `elemLocalRdrEnv` name_env) ]
= do { let (kv_bndrs, tv_bndrs) = extractHsTyRdrTyVars ty
; checkHsBndrFlags is_type doc ty tv_bndrs
; tv_names <- newLocalBndrsRn [L loc tv | tv <- tv_bndrs]
; bindLocalNamesFV tv_names $ do
{ (ty', fvs1) <- rnLHsTyKi is_type doc ty
; (res, fvs2) <- thing_inside (HsBSig ty' tv_names)
; name_env <- getLocalRdrEnv
; tv_names <- newLocalBndrsRn [L loc tv | tv <- tv_bndrs
, not (tv `elemLocalRdrEnv` name_env) ]
; kv_names <- newLocalBndrsRn [L loc kv | kv <- kv_bndrs
, not (kv `elemLocalRdrEnv` name_env) ]
; bindLocalNamesFV kv_names $
bindLocalNamesFV tv_names $
do { (ty', fvs1) <- rnLHsTyKi is_type doc ty
; (res, fvs2) <- thing_inside (HsBSig ty' (kv_names, tv_names))
; return (res, fvs1 `plusFV` fvs2) } }
checkHsBndrFlags :: Bool -> HsDocContext
......@@ -853,3 +861,104 @@ checkTH e what -- Raise an error in a stage-1 compiler
nest 2 (ppr e)])
#endif
\end{code}
%************************************************************************
%* *
Finding the free type variables of a (HsType RdrName)
%* *
%************************************************************************
extractHsTyRdrNames finds the free variables of a HsType
It's used when making the for-alls explicit.
Note [Kind and type-variable binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a type signature we may implicitly bind type varaible and, more
recently, kind variables. For example:
* f :: a -> a
f = ...
Here we need to find the free type variables of (a -> a),
so that we know what to quantify
* class C (a :: k) where ...
This binds 'k' in ..., as well as 'a'
* f (x :: a -> [a]) = ....
Here we bind 'a' in ....
* f (x :: T a -> T (b :: k)) = ...
Here we bind both 'a' and the kind variable 'k'
* type instance F (T (a :: Maybe k)) = ...a...k...
Here we want to constrain the kind of 'a', and bind 'k'.
In general we want to walk over a type, and find
* Its free type variables
* The free kind variables of any kind signatures in the type
Hence we returns a pair (kind-vars, type vars)
See also Note [HsBSig binder lists] in HsTypes
\begin{code}
type FreeKiTyVars = ([RdrName], [RdrName])
extractHsTyRdrTyVars :: LHsType RdrName -> FreeKiTyVars
-- See Note [Kind and type-variable binders]
extractHsTyRdrTyVars ty
= case extract_lty ty ([],[]) of
(kvs, tvs) -> (nub kvs, nub tvs)
extractHsTysRdrTyVars :: [LHsType RdrName] -> FreeKiTyVars
-- See Note [Kind and type-variable binders]
extractHsTysRdrTyVars ty
= case extract_ltys ty ([],[]) of
(kvs, tvs) -> (nub kvs, nub tvs)
extract_lctxt :: LHsContext RdrName -> FreeKiTyVars -> FreeKiTyVars
extract_lctxt ctxt acc = foldr extract_lty acc (unLoc ctxt)
extract_ltys :: [LHsType RdrName] -> FreeKiTyVars -> FreeKiTyVars
extract_ltys tys acc = foldr extract_lty acc tys
extract_lty :: LHsType RdrName -> FreeKiTyVars -> FreeKiTyVars
extract_lty (L _ ty) acc
= case ty of
HsTyVar tv -> extract_tv tv acc
HsBangTy _ ty -> extract_lty ty acc
HsRecTy flds -> foldr (extract_lty . cd_fld_type) acc flds
HsAppTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsListTy ty -> extract_lty ty acc
HsPArrTy ty -> extract_lty ty acc
HsTupleTy _ tys -> extract_ltys tys acc
HsFunTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsIParamTy _ ty -> extract_lty ty acc
HsEqTy ty1 ty2 -> extract_lty ty1 (extract_lty ty2 acc)
HsOpTy ty1 (_, (L _ tv)) ty2 -> extract_tv tv (extract_lty ty1 (extract_lty ty2 acc))
HsParTy ty -> extract_lty ty acc
HsCoreTy {} -> acc -- The type is closed
HsQuasiQuoteTy {} -> acc -- Quasi quotes mention no type variables
HsSpliceTy {} -> acc -- Type splices mention no type variables
HsDocTy ty _ -> extract_lty ty acc
HsExplicitListTy _ tys -> extract_ltys tys acc
HsExplicitTupleTy _ tys -> extract_ltys tys acc
HsTyLit _ -> acc
HsWrapTy _ _ -> panic "extract_lty"
HsKindSig ty ki -> case extract_lty ty acc of { (kvs1, tvs) ->
case extract_lty ki ([],kvs1) of { (_, kvs2) ->
-- Kinds shouldn't have sort signatures!
(kvs2, tvs) }}
HsForAllTy _ [] cx ty -> extract_lctxt cx (extract_lty ty acc)
HsForAllTy _ tvs cx ty -> (acc_kvs ++ body_kvs,
acc_tvs ++ filterOut (`elem` locals_tvs) body_tvs)
where
(body_kvs, body_tvs) = extract_lctxt cx (extract_lty ty ([],[]))
(acc_kvs, acc_tvs) = acc
locals_tvs = hsLTyVarNames tvs
-- Currently we don't have a syntax to explicity bind
-- kind variables, so these are all type variables
extract_tv :: RdrName -> FreeKiTyVars -> FreeKiTyVars
extract_tv tv acc
| isRdrTyVar tv = case acc of (kvs,tvs) -> (kvs, tv : tvs)
| otherwise = acc
\end{code}
......@@ -70,7 +70,6 @@ import TysWiredIn
import BasicTypes
import SrcLoc
import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
import Util
import UniqSupply
import Outputable
import FastString
......@@ -793,7 +792,7 @@ bindScopedKindVars hs_tvs thing_inside
where
kvs :: [KindVar] -- All skolems
kvs = [ mkKindSigVar kv
| L _ (KindedTyVar _ (HsBSig _ kvs)) <- hs_tvs
| L _ (KindedTyVar _ (HsBSig _ (_, kvs))) <- hs_tvs
, kv <- kvs ]
tcHsTyVarBndrs :: [LHsTyVarBndr Name]
......@@ -1071,23 +1070,33 @@ Historical note:
\begin{code}
tcHsPatSigType :: UserTypeCtxt
-> HsBndrSig (LHsType Name) -- The type signature
-> TcM ([TyVar], -- Newly in-scope type variables
Type) -- The signature
-> TcM ( Type -- The signature
, [(Name, TcTyVar)] ) -- The new bit of type environment, binding
-- the scoped type variables
-- Used for type-checking type signatures in
-- (a) patterns e.g f (x::Int) = e
-- (b) result signatures e.g. g x :: Int = e
-- (c) RULE forall bndrs e.g. forall (x::Int). f x = x
tcHsPatSigType ctxt (HsBSig hs_ty sig_tvs)
tcHsPatSigType ctxt (HsBSig hs_ty (sig_kvs, sig_tvs))
= addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
do { let new_tv name = do { kind <- newMetaKindVar
; return (mkTyVar name kind) }
do { kvs <- mapM new_kv sig_kvs
; tvs <- mapM new_tv sig_tvs
; sig_ty <- tcExtendTyVarEnv tvs $
; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
tcHsLiftedType hs_ty
; sig_ty <- zonkTcType sig_ty
; checkValidType ctxt sig_ty
; return (tvs, sig_ty) }
; return (sig_ty, ktv_binds) }
where
new_kv name = new_tkv name superKind
new_tv name = do { kind <- newMetaKindVar
; new_tkv name kind }
new_tkv name kind -- See Note [Pattern signature binders]
= case ctxt of
RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
_ -> newSigTyVar name kind -- See Note [Unifying SigTvs]
tcPatSig :: UserTypeCtxt
-> HsBndrSig (LHsType Name)
......@@ -1098,7 +1107,7 @@ tcPatSig :: UserTypeCtxt
HsWrapper) -- Coercion due to unification with actual ty
-- Of shape: res_ty ~ sig_ty
tcPatSig ctxt sig res_ty
= do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
= do { (sig_ty, sig_tvs) <- tcHsPatSigType ctxt sig
-- sig_tvs are the type variables free in 'sig',
-- and not already in scope. These are the ones
-- that should be brought into scope
......@@ -1125,45 +1134,65 @@ tcPatSig ctxt sig res_ty
-- f :: Int -> Int
-- f (x :: T a) = ...
-- Here 'a' doesn't get a binding. Sigh
; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
; let bad_tvs = [ tv | (_, tv) <- sig_tvs
, not (tv `elemVarSet` exactTyVarsOfType sig_ty) ]
; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
-- Now do a subsumption check of the pattern signature against res_ty
; (subst, sig_tvs') <- tcInstSigTyVars sig_tvs
; let sig_ty' = substTy subst sig_ty
; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
-- Check that each is bound to a distinct type variable,
-- and one that is not already in scope
; binds_in_scope <- getScopedTyVarBinds
; let tv_binds :: [(Name,TcTyVar)]
tv_binds = map tyVarName sig_tvs `zip` sig_tvs'
; check binds_in_scope tv_binds
; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
-- Phew!
; return (sig_ty', tv_binds, wrap)
; return (sig_ty, sig_tvs, wrap)
} }
where
check :: [(Name,TcTyVar)] -> [(Name, TcTyVar)] -> TcM ()
check _ [] = return ()
check in_scope ((n,tv):rest) = do { check_one in_scope n tv
; check ((n,tv):in_scope) rest }
check_one :: [(Name,TcTyVar)] -> Name -> TcTyVar -> TcM ()
check_one in_scope n tv
= checkTc (null dups) (dupInScope n (head dups) tv)
-- Must not bind to the same type variable
-- as some other in-scope type variable
where
dups = [n' | (n',tv') <- in_scope, tv' == tv]
patBindSigErr :: [TyVar] -> SDoc
patBindSigErr :: [(Name, TcTyVar)] -> SDoc
patBindSigErr sig_tvs
= hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
<+> pprQuotedList sig_tvs)
<+> pprQuotedList (map fst sig_tvs))
2 (ptext (sLit "in a pattern binding signature"))
\end{code}
Note [Pattern signature binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T = forall a. T a (a->Int)
f (T x (f :: a->Int) = blah)
Here
* The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
It must be a skolem so that that it retains its identity, and
TcErrors.getSkolemInfo can therreby find the binding site for the skolem.
* The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
* Then unificaiton makes a_sig := a_sk
That's why we must make a_sig a SigTv, not a SkolemTv, so that it can unify to a_sk.
For RULE binders, though, things are a bit different (yuk).
RULE "foo" forall (x::a) (y::[a]). f x y = ...
Here this really is the binding site of the type variable so we'd like
to use a skolem, so that we get a complaint if we unify two of them
together.
Note [Unifying SigTvs]
~~~~~~~~~~~~~~~~~~~~~~
ALAS we have no decent way of avoiding two SigTvs getting unified.
Consider
f (x::(a,b)) (y::c)) = [fst x, y]
Here we'd really like to complain that 'a' and 'c' are unified. But
for the reasons above we can't make a,b,c into skolems, so they
are just SigTvs that can unify. And indeed, this would be ok,
f x (y::c) = case x of
(x1 :: a1, True) -> [x,y]
(x1 :: a2, False) -> [x,y,y]
Here the type of x's first component is called 'a1' in one branch and
'a2' in the other. We could try insisting on the same OccName, but
they definitely won't have the sane lexical Name.
I think we could solve this by recording in a SigTv a list of all the
in-scope varaibles that it should not unify with, but it's fiddly.
%************************************************************************
%* *
......@@ -1394,11 +1423,5 @@ badPatSigTvs sig_ty bad_tvs
ptext (sLit "but are actually discarded by a type synonym") ]
, ptext (sLit "To fix this, expand the type synonym")
, ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
dupInScope :: Name -> Name -> TcTyVar -> SDoc
dupInScope n n' _
= hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
2 (vcat [ptext (sLit "are bound to the same type (variable)"),
ptext (sLit "Distinct scoped type variables must be distinct")])
\end{code}
......@@ -40,7 +40,7 @@ module TcMType (
--------------------------------
-- Instantiation
tcInstTyVars, tcInstSigTyVars,
tcInstTyVars, tcInstSigTyVars, newSigTyVar,
tcInstType,
tcInstSkolTyVars, tcInstSuperSkolTyVars,
tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
......@@ -61,7 +61,7 @@ module TcMType (
-- Zonking
zonkType, zonkKind, zonkTcPredType,
skolemiseSigTv, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkSigTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
......@@ -270,14 +270,17 @@ tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
tcInstSigTyVar subst tv
= do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tv) uniq
; let name' = setNameUnique name uniq
-- Use the same OccName so that the tidy-er
-- doesn't rename 'a' to 'a0' etc
kind = substTy subst (tyVarKind tv)
new_tv = mkTcTyVar name kind (MetaTv SigTv ref)
; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
; return (mkTcTyVar name' kind (MetaTv SigTv ref)) }
\end{code}
Note [Kind substitution when instantiating]
......@@ -448,27 +451,6 @@ tcInstTyVarX subst tyvar
\end{code}
%************************************************************************
%* *
MetaTvs: SigTvs
%* *
%************************************************************************
\begin{code}
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
zonkSigTyVar sig_tv
| isSkolemTyVar sig_tv
= return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
| otherwise
= ASSERT( isSigTyVar sig_tv )
do { ty <- zonkTcTyVar sig_tv
; return (tcGetTyVar "zonkSigTyVar" ty) }
-- 'ty' is bound to be a type variable, because SigTvs
-- can only be unified with type variables
\end{code}