Commit 716c2ae4 authored by ian@well-typed.com's avatar ian@well-typed.com
Browse files

Merge branch 'master' of http://darcs.haskell.org/ghc

parents 31b2706c 6ecfa98d
......@@ -685,6 +685,7 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
arg_tys' = substTys tenv arg_tys
; traceTc "tcConPat" (ppr con_name $$ ppr ex_tvs' $$ ppr pat_ty' $$ ppr arg_tys')
; if null ex_tvs && null eq_spec && null theta
then do { -- The common case; no class bindings etc
-- (see Note [Arrows and patterns])
......
......@@ -23,6 +23,7 @@ import TcMType as TcM
import TcType
import TcSMonad as TcS
import TcInteract
import Kind ( defaultKind_maybe )
import Inst
import FunDeps ( growThetaTyVars )
import Type ( classifyPredType, PredTree(..), getClassPredTys_maybe )
......@@ -782,7 +783,7 @@ defaultTyVar :: TcTyVar -> TcS TcTyVar
-- Precondition: MetaTyVars only
-- See Note [DefaultTyVar]
defaultTyVar the_tv
| not (k `eqKind` default_k)
| Just default_k <- defaultKind_maybe (tyVarKind the_tv)
= do { tv' <- TcS.cloneMetaTyVar the_tv
; let new_tv = setTyVarKind tv' default_k
; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
......@@ -793,9 +794,6 @@ defaultTyVar the_tv
-- We keep the same Untouchables on tv'
| otherwise = return the_tv -- The common case
where
k = tyVarKind the_tv
default_k = defaultKind k
approximateWC :: WantedConstraints -> Cts
-- Postcondition: Wanted or Derived Cts
......
......@@ -992,42 +992,42 @@ consUseH98Syntax _ = True
-----------------------------------
tcConDecls :: NewOrData -> TyCon -> ([TyVar], Type)
-> [LConDecl Name] -> TcM [DataCon]
tcConDecls new_or_data rep_tycon res_tmpl cons
= mapM (addLocM (tcConDecl new_or_data rep_tycon res_tmpl)) cons
tcConDecls new_or_data rep_tycon (tmpl_tvs, res_tmpl) cons
= mapM (addLocM $ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl) cons
tcConDecl :: NewOrData
-> TyCon -- Representation tycon
-> ([TyVar], Type) -- Return type template (with its template tyvars)
-- (tvs, T tys), where T is the family TyCon
-> TyCon -- Representation tycon
-> [TyVar] -> Type -- Return type template (with its template tyvars)
-- (tvs, T tys), where T is the family TyCon
-> ConDecl Name
-> TcM DataCon
tcConDecl new_or_data rep_tycon res_tmpl -- Data types
tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl -- Data types
(ConDecl { con_name = name
, con_qvars = hs_tvs, con_cxt = hs_ctxt
, con_details = hs_details, con_res = hs_res_ty })
= addErrCtxt (dataConCtxt name) $
do { traceTc "tcConDecl 1" (ppr name)
; (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts)
<- tcHsTyVarBndrs hs_tvs $ \ tvs ->
; (ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts)
<- tcHsTyVarBndrs hs_tvs $ \ _ ->
do { ctxt <- tcHsContext hs_ctxt
; details <- tcConArgs new_or_data hs_details
; res_ty <- tcConRes hs_res_ty
; let (is_infix, field_lbls, btys) = details
(arg_tys, stricts) = unzip btys
; return (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
; return (ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
-- Generalise the kind variables (returning quantifed TcKindVars)
-- and quantify the type variables (substituting their kinds)
-- REMEMBER: 'tvs' and 'tkvs' are:
-- REMEMBER: 'tkvs' are:
-- ResTyH98: the *existential* type variables only
-- ResTyGADT: *all* the quantified type variables
-- c.f. the comment on con_qvars in HsDecls
; tkvs <- case (res_ty, res_tmpl) of
(ResTyH98, (tvs, _)) -> quantifyTyVars (mkVarSet tvs) (tyVarsOfTypes arg_tys)
(ResTyGADT ty, _) -> quantifyTyVars emptyVarSet (tyVarsOfTypes (ty:arg_tys))
; tkvs <- case res_ty of
ResTyH98 -> quantifyTyVars (mkVarSet tmpl_tvs) (tyVarsOfTypes (ctxt++arg_tys))
ResTyGADT res_ty -> quantifyTyVars emptyVarSet (tyVarsOfTypes (res_ty:ctxt++arg_tys))
; traceTc "tcConDecl" (ppr name $$ ppr arg_tys $$ ppr tvs $$ ppr tkvs)
; traceTc "tcConDecl" (ppr name $$ ppr arg_tys $$ ppr tkvs)
-- Zonk to Types
; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
......@@ -1037,9 +1037,8 @@ tcConDecl new_or_data rep_tycon res_tmpl -- Data types
ResTyH98 -> return ResTyH98
ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes res_tmpl qtkvs res_ty
; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes tmpl_tvs res_tmpl qtkvs res_ty
; traceTc "tcConDecl 3" (vcat [ppr name, ppr tkvs, ppr qtkvs, ppr univ_tvs, ppr ex_tvs])
; fam_envs <- tcGetFamInstEnvs
; buildDataCon fam_envs (unLoc name) is_infix
stricts field_lbls
......@@ -1086,7 +1085,7 @@ tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
-- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
-- In this case orig_res_ty = T (e,e)
rejigConRes :: ([TyVar], Type) -- Template for result type; e.g.
rejigConRes :: [TyVar] -> Type -- Template for result type; e.g.
-- data instance T [a] b c = ...
-- gives template ([a,b,c], T [a] b c)
-> [TyVar] -- where MkT :: forall x y z. ...
......@@ -1099,13 +1098,13 @@ rejigConRes :: ([TyVar], Type) -- Template for result type; e.g.
-- the same as the parent tycon, because we are in the middle
-- of a recursive knot; so it's postponed until checkValidDataCon
rejigConRes (tmpl_tvs, res_ty) dc_tvs ResTyH98
rejigConRes tmpl_tvs res_ty dc_tvs ResTyH98
= (tmpl_tvs, dc_tvs, [], res_ty)
-- In H98 syntax the dc_tvs are the existential ones
-- data T a b c = forall d e. MkT ...
-- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
rejigConRes tmpl_tvs res_tmpl dc_tvs (ResTyGADT res_ty)
-- E.g. data T [a] b c where
-- MkT :: forall x y z. T [(x,y)] z z
-- Then we generate
......
......@@ -1115,7 +1115,53 @@ lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
%* *
%************************************************************************
Note [Lifting coercions over types: liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The KPUSH rule deals with this situation
data T a = MkK (a -> Maybe a)
g :: T t1 ~ K t2
x :: t1 -> Maybe t1
case (K @t1 x) |> g of
K (y:t2 -> Maybe t2) -> rhs
We want to push the coercion inside the constructor application.
So we do this
g' :: t1~t2 = Nth 0 g
case K @t2 (x |> g' -> Maybe g') of
K (y:t2 -> Maybe t2) -> rhs
The crucial operation is that we
* take the type of K's argument: a -> Maybe a
* and substitute g' for a
thus giving *coercion*. This is what liftCoSubst does.
Note [Substituting kinds in liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to take care with kind polymorphism. Suppose
K :: forall k (a:k). (forall b:k. a -> b) -> T k a
Now given (K @kk1 @ty1 v) |> g) where
g :: T kk1 ty1 ~ T kk2 ty2
we want to compute
(forall b:k a->b) [ Nth 0 g/k, Nth 1 g/a ]
Notice that we MUST substitute for 'k'; this happens in
liftCoSubstTyVarBndr. But what should we substitute?
We need to take b's kind 'k' and return a Kind, not a Coercion!
Happily we can do this because we know that all kind coercions
((Nth 0 g) in this case) are Refl. So we need a special purpose
subst_kind: LiftCoSubst -> Kind -> Kind
that expects a Refl coercion (or something equivalent to Refl)
when it looks up a kind variable.
\begin{code}
-- ----------------------------------------------------
-- See Note [Lifting coercions over types: liftCoSubst]
-- ----------------------------------------------------
data LiftCoSubst = LCS InScopeSet LiftCoEnv
type LiftCoEnv = VarEnv Coercion
......@@ -1158,14 +1204,44 @@ liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv
liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
= (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
where
new_cenv | no_change = delVarEnv cenv old_var
| otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
no_change = new_var == old_var
new_var = uniqAway in_scope old_var
no_change = no_kind_change && (new_var == old_var)
new_var1 = uniqAway in_scope old_var
old_ki = tyVarKind old_var
no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
new_var | no_kind_change = new_var1
| otherwise = setTyVarKind new_var1 (subst_kind subst old_ki)
subst_kind :: LiftCoSubst -> Kind -> Kind
-- See Note [Substituting kinds in liftCoSubst]
subst_kind subst@(LCS _ cenv) kind
= go kind
where
go (LitTy n) = n `seq` LitTy n
go (TyVarTy kv) = subst_kv kv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
go (ForAllTy tv ty) = case liftCoSubstTyVarBndr subst tv of
(subst', tv') ->
ForAllTy tv' $! (subst_kind subst' ty)
subst_kv kv
| Just co <- lookupVarEnv cenv kv
, let co_kind = coercionKind co
= ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
pFst co_kind
| otherwise
= TyVarTy kv
\end{code}
\begin{code}
......
......@@ -40,10 +40,10 @@ module Kind (
isAnyKind, isAnyKindCon,
okArrowArgKind, okArrowResultKind,
isSubOpenTypeKind,
isSubOpenTypeKind, isSubOpenTypeKindKey,
isSubKind, isSubKindCon,
tcIsSubKind, tcIsSubKindCon,
defaultKind,
defaultKind, defaultKind_maybe,
-- ** Functions on variables
kiVarsOfKind, kiVarsOfKinds
......@@ -60,6 +60,7 @@ import TyCon
import VarSet
import PrelNames
import Outputable
import Maybes( orElse )
import Util
\end{code}
......@@ -172,13 +173,8 @@ returnsConstraintKind _ = False
-- arg -> res
okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
okArrowArgKindCon kc
| isLiftedTypeKindCon kc = True
| isUnliftedTypeKindCon kc = True
| isConstraintKindCon kc = True
| otherwise = False
okArrowResultKindCon = okArrowArgKindCon
okArrowArgKindCon = isSubOpenTypeKindCon
okArrowResultKindCon = isSubOpenTypeKindCon
okArrowArgKind, okArrowResultKind :: Kind -> Bool
okArrowArgKind (TyConApp kc []) = okArrowArgKindCon kc
......@@ -198,14 +194,17 @@ isSubOpenTypeKind :: Kind -> Bool
isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
isSubOpenTypeKind _ = False
isSubOpenTypeKindCon kc
= isOpenTypeKindCon kc
|| isUnliftedTypeKindCon kc
|| isLiftedTypeKindCon kc
|| isConstraintKindCon kc -- Needed for error (Num a) "blah"
-- and so that (Ord a -> Eq a) is well-kinded
-- and so that (# Eq a, Ord b #) is well-kinded
-- See Note [Kind Constraint and kind *]
isSubOpenTypeKindCon kc = isSubOpenTypeKindKey (tyConUnique kc)
isSubOpenTypeKindKey :: Unique -> Bool
isSubOpenTypeKindKey uniq
= uniq == openTypeKindTyConKey
|| uniq == unliftedTypeKindTyConKey
|| uniq == liftedTypeKindTyConKey
|| uniq == constraintKindTyConKey -- Needed for error (Num a) "blah"
-- and so that (Ord a -> Eq a) is well-kinded
-- and so that (# Eq a, Ord b #) is well-kinded
-- See Note [Kind Constraint and kind *]
-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
......@@ -271,7 +270,8 @@ tcIsSubKindCon kc1 kc2
| otherwise = isSubKindCon kc1 kc2
-------------------------
defaultKind :: Kind -> Kind
defaultKind :: Kind -> Kind
defaultKind_maybe :: Kind -> Maybe Kind
-- ^ Used when generalising: default OpenKind and ArgKind to *.
-- See "Type#kind_subtyping" for more information on what that means
......@@ -289,9 +289,11 @@ defaultKind :: Kind -> Kind
-- This defaulting is done in TcMType.zonkTcTyVarBndr.
--
-- The test is really whether the kind is strictly above '*'
defaultKind (TyConApp kc _args)
| isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
defaultKind k = k
defaultKind_maybe (TyConApp kc _args)
| isOpenTypeKindCon kc = ASSERT( null _args ) Just liftedTypeKind
defaultKind_maybe _ = Nothing
defaultKind k = defaultKind_maybe k `orElse` k
-- Returns the free kind variables in a kind
kiVarsOfKind :: Kind -> VarSet
......
......@@ -159,7 +159,7 @@ import Class
import TyCon
import TysPrim
import {-# SOURCE #-} TysWiredIn ( eqTyCon, typeNatKind, typeSymbolKind )
import PrelNames ( eqTyConKey, ipClassNameKey,
import PrelNames ( eqTyConKey, ipClassNameKey, openTypeKindTyConKey,
constraintKindTyConKey, liftedTypeKindTyConKey )
import CoAxiom
......@@ -1216,7 +1216,7 @@ cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
-- So the RHS has a data type
cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX env (tyVarKind tv1) (tyVarKind tv1)
cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2)
`thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
......@@ -1257,7 +1257,13 @@ cmpTypesX _ _ [] = GT
cmpTc :: TyCon -> TyCon -> Ordering
-- Here we treat * and Constraint as equal
-- See Note [Kind Constraint and kind *] in Kinds.lhs
cmpTc tc1 tc2 = nu1 `compare` nu2
--
-- Also we treat OpenTypeKind as equal to either * or #
-- See Note [Comparison with OpenTypeKind]
cmpTc tc1 tc2
| u1 == openTypeKindTyConKey, isSubOpenTypeKindKey u2 = EQ
| u2 == openTypeKindTyConKey, isSubOpenTypeKindKey u1 = EQ
| otherwise = nu1 `compare` nu2
where
u1 = tyConUnique tc1
nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
......@@ -1265,6 +1271,18 @@ cmpTc tc1 tc2 = nu1 `compare` nu2
nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
\end{code}
Note [Comparison with OpenTypeKind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In PrimOpWrappers we have things like
PrimOpWrappers.mkWeak# = /\ a b c. Prim.mkWeak# a b c
where
Prim.mkWeak# :: forall (a:Open) b c. a -> b -> c
-> State# RealWorld -> (# State# RealWorld, Weak# b #)
Now, eta reduction will turn the definition into
PrimOpWrappers.mkWeak# = Prim.mkWeak#
which is kind-of OK, but now the types aren't really equal. So HACK HACK
we pretend (in Core) that Open is equal to * or #. I hate this.
Note [cmpTypeX]
~~~~~~~~~~~~~~~
......
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