Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : ghc-kinds
http://hackage.haskell.org/trac/ghc/changeset/cf145bf954424e5e3f6f6198511e69043010b482 >--------------------------------------------------------------- commit cf145bf954424e5e3f6f6198511e69043010b482 Author: Simon Peyton Jones <[email protected]> Date: Thu Oct 27 09:52:41 2011 +0100 Wibbles with Simon >--------------------------------------------------------------- compiler/typecheck/FamInst.lhs | 1 + compiler/typecheck/TcHsType.lhs | 7 +++++-- compiler/typecheck/TcMType.lhs | 16 ++++++++++------ compiler/typecheck/TcTyClsDecls.lhs | 2 +- compiler/types/FamInstEnv.lhs | 22 ++++++++++++++++------ 5 files changed, 33 insertions(+), 15 deletions(-) diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index 39f5cda..e0e102a 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -248,6 +248,7 @@ addLocalFamInst home_fie famInst = do -- If there are any conflicts, we should probably error -- But, if we're allowed to overwrite and the conflict is in the home FIE, -- then overwrite instead of error. + traceTc "checkForConflicts" (ppr conflicts $$ ppr famInst $$ ppr inst_envs) isGHCi <- getIsGHCi case conflicts of dup : _ -> case (isGHCi, home_conflicts) of diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index e9b73e8..cf6c4aa 100755 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -256,6 +256,7 @@ tcHsKindedType hs_ty = dsHsType hs_ty tcHsBangType :: LHsType Name -> TcM Type -- Permit a bang, but discard it +-- Input type has already been kind-checked tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty tcHsBangType ty = tcHsKindedType ty @@ -328,7 +329,8 @@ kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind -- This is the general case: infer the kind and compare kc_check_hs_type ty exp_kind - = do { (ty', act_kind) <- kc_hs_type ty + = do { traceTc "kc_check_hs_type" (ppr ty) + ; (ty', act_kind) <- kc_hs_type ty -- Add the context round the inner check only -- because checkExpectedKind already mentions -- 'ty' by name in any error message @@ -356,7 +358,8 @@ kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty) kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind) kc_lhs_type (L span ty) = setSrcSpan span $ - do { (ty', kind) <- kc_hs_type ty + do { traceTc "kc_lhs_type" (ppr ty) + ; (ty', kind) <- kc_hs_type ty ; return (L span ty', kind) } -- kc_hs_type *returns* the kind of the type, rather than taking an expected diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index e90f617..fd5b5b8 100755 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -570,12 +570,13 @@ zonkTcPredType = zonkTcType \begin{code} zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars tyvars - = do { z_kvs <- mapM zonkQuantifiedTyVar kvs + = do { let (kvs, tvs) = splitKiTyVars tyvars + ; z_kvs <- mapM zonkQuantifiedTyVar kvs ; z_tvs <- mapM zonkQuantifiedTyVar tvs - ; let subst = zipOpenTvSubst kvs (map mkTyVarTy z_kvs) - zs_tvs = map (updateTyVarKind (substTy subst)) z_tvs - ; return $ z_kvs ++ zs_tvs } - where (kvs, tvs) = splitKiTyVars tyvars + -- By doing the kind variables first, we ensure that + -- any kind variables mentioned in the kinds of the + -- type variables refer to the now-quantified versions + ; return $ z_kvs ++ z_tvs } zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- The quantified type variables often include meta type variables @@ -619,9 +620,12 @@ skolemiseUnboundMetaTyVar tv details do { span <- getSrcSpanM -- Get the location from "here" -- ie where we are generalising ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land - ; let final_kind = defaultKind (tyVarKind tv) + ; kind <- zonkTcKind (tyVarKind tv) + ; let final_kind = defaultKind kind final_name = mkInternalName uniq (getOccName tv) span final_tv = mkTcTyVar final_name final_kind details + + -- JPM: combine writeMetaKindVar, writeMetaTyVar ; (if isSuperKind final_kind then writeMetaKindVar else writeMetaTyVar) tv (mkTyVarTy final_tv) diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 68b095d..88d6455 100755 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -855,7 +855,7 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types <- kcConDecl new_or_data con ; addErrCtxt (dataConCtxt name) $ tcTyVarBndrsKindGen tvs $ \ tvs' -> do - { ctxt' <- tcHsKindedContext =<< kcHsContext ctxt + { ctxt' <- tcHsKindedContext ctxt ; checkTc (existential_ok || conRepresentibleWithH98Syntax con) (badExistential name) ; traceTc "tcConDecl 1" (ppr con) diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index 82c934d..348adaf 100755 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -386,12 +386,7 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs Just subst | conflicting old_fam_inst subst -> Just subst _other -> Nothing - -- - In the case of data family instances, any overlap is fundamentally a - -- conflict (as these instances imply injective type mappings). - -- - In the case of type family instances, overlap is admitted as long as - -- the right-hand sides of the overlapping rules coincide under the - -- overlap substitution. We require that they are syntactically equal; - -- anything else would be difficult to test for at this stage. + -- Note [Family instance overlap conflicts] conflicting old_fam_inst subst | isAlgTyCon fam = True | otherwise = not (old_rhs `eqType` new_rhs) @@ -402,6 +397,21 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs) \end{code} +Note [Family instance overlap conflicts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +- In the case of data family instances, any overlap is fundamentally a + conflict (as these instances imply injective type mappings). + +- In the case of type family instances, overlap is admitted as long as + the right-hand sides of the overlapping rules coincide under the + overlap substitution. eg + type instance F a Int = a + type instance F Int b = b + These two overlap on (F Int Int) but then both RHSs are Int, + so all is well. We require that they are syntactically equal; + anything else would be difficult to test for at this stage. + + While @lookupFamInstEnv@ uses a one-way match, the next function @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is needed to check for overlapping instances. _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
