From: Tim Chevalier Date: Tue, 22 Apr 2008 01:56:22 +0000 (+0000) Subject: External Core typechecker - improve handling of coercions X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=10704b34c1928dde3d0ef33fe37c3eb7b948975f External Core typechecker - improve handling of coercions Reorganized coercion-related code in the typechecker (this was brought about by typechecking the Core versions of the optimized GHC libraries.) A few miscellaneous changes (fixed a bug in Prep involving eta-expanding partial applications that had additional type arguments.) --- diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index 95c7281..cab3e62 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -91,7 +91,8 @@ checkModule globalEnv (Module mn tdefs vdefgs) = vdefgs return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))) - (mn, globalEnv) + -- avoid name shadowing + (mn, eremove globalEnv mn) -- Like checkModule, but doesn't typecheck the code, instead just -- returning declared types for top-level defns. @@ -229,51 +230,44 @@ mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv) -checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = +checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do + mn <- getMname case vdefg of Rec vdefs -> - do e_venv' <- foldM extendVenv e_venv e_vts - l_venv' <- foldM extendVenv l_venv l_vts + do (e_venv', l_venv') <- makeEnv mn vdefs let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') - mapM_ (\ (vdef@(Vdef ((m,_),t,e))) -> - do mn <- getMname - requireModulesEq m mn "value definition" vdef True - k <- checkTy (tcenv,tvenv) t - require (k `eqKind` Klifted) ("unlifted kind in:\n" ++ show vdef) - t' <- checkExp env' e - requireM (equalTy tsenv t t') - ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t')) vdefs - return (e_venv',l_venv') - where e_vts = [ (v,t) | Vdef ((Just _,v),t,_) <- vdefs ] - l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs] - Nonrec (vdef@(Vdef ((m,v),t,e))) -> - do mn <- getMname - -- TODO: document this weirdness - let isZcMain = vdefIsMainWrapper mn m - unless isZcMain $ - requireModulesEq m mn "value definition" vdef True - k <- checkTy (tcenv,tvenv) t - require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef) - require ((not top_level) || (not (k `eqKind` Kunlifted))) - ("top-level unlifted kind in:\n" ++ show vdef) - t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e - requireM (equalTy tsenv t t') - ("declared type doesn't match expression type in:\n" - ++ show vdef ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t') - if isNothing m then - do l_venv' <- extendVenv l_venv (v,t) - return (e_venv,l_venv') - else - -- awful, but avoids name shadowing -- - -- otherwise we'd have two bindings for "main" - do e_venv' <- if isZcMain - then return e_venv - else extendVenv e_venv (v,t) - return (e_venv',l_venv) + mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) + ("unlifted kind in:\n" ++ show vdef)) env') + vdefs + return (e_venv', l_venv') + Nonrec vdef -> + do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv) + checkVdef (\ vdef k -> do + require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef) + require ((not top_level) || (not (k `eqKind` Kunlifted))) + ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef + makeEnv mn [vdef] + + where makeEnv mn vdefs = do + ev <- foldM extendVenv e_venv e_vts + lv <- foldM extendVenv l_venv l_vts + return (ev, lv) + where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs, + not (vdefIsMainWrapper mn (Just m))] + l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs] + checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do + mn <- getMname + let isZcMain = vdefIsMainWrapper mn m + unless isZcMain $ + requireModulesEq m mn "value definition" vdef True + k <- checkTy (tcenv,tvenv) t + checkKind vdef k + t' <- checkExp env e + requireM (equalTy tsenv t t') + ("declared type doesn't match expression type in:\n" + ++ show vdef ++ "\n" ++ + "declared type: " ++ show t ++ "\n" ++ + "expression type: " ++ show t') vdefIsMainWrapper :: AnMname -> Mname -> Bool vdefIsMainWrapper enclosing defining = @@ -393,15 +387,11 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch return t c@(Cast e t) -> do eTy <- ch e - k <- checkTy (tcenv,tvenv) t - case k of - (Keq fromTy toTy) -> do - require (eTy == fromTy) ("Type mismatch in cast: c = " - ++ show c ++ " and " ++ show eTy - ++ " and " ++ show fromTy) - return toTy - _ -> fail ("Cast with non-equality kind: " ++ show e - ++ " and " ++ show t ++ " has kind " ++ show k) + (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t + require (eTy == fromTy) ("Type mismatch in cast: c = " + ++ show c ++ "\nand eTy = " ++ show eTy + ++ "\n and " ++ show fromTy) + return toTy Note _ e -> ch e External _ t -> @@ -466,7 +456,7 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch checkExp env e checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind -checkTy es@(tcenv,tvenv) t = ch t +checkTy es@(tcenv,tvenv) = ch where ch (Tvar tv) = lookupM tvenv tv ch (Tcon qtc) = do @@ -495,7 +485,7 @@ checkTy es@(tcenv,tvenv) t = ch t -- :Co:TTypeable2 (->) -- where in this case, :Co:TTypeable2 expects an -- argument of kind (*->(*->*)) and (->) has kind - -- (?->(?->*)). In general, I don't think it's + -- (?->(?->*)). I'm not sure whether or not it's -- sound to apply an arbitrary coercion to an -- argument that's a subkind of what it expects. then warn $ "Applying coercion " ++ show tc ++ @@ -507,23 +497,12 @@ checkTy es@(tcenv,tvenv) t = ch t return $ Keq (substl tvs tys from) (substl tvs tys to) Nothing -> checkTapp t1 t2 where checkTapp t1 t2 = do - k1 <- ch t1 + k1 <- ch t1 k2 <- ch t2 case k1 of - Karrow k11 k12 -> - case k2 of - Keq eqTy1 eqTy2 -> do - -- Distribute the type operator over the - -- coercion - subK1 <- checkTy es eqTy1 - subK2 <- checkTy es eqTy2 - require (subK2 `subKindOf` k11 && - subK1 `subKindOf` k11) $ - kindError - return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2) - _ -> do - require (k2 `subKindOf` k11) kindError - return k12 + Karrow k11 k12 -> do + require (k2 `subKindOf` k11) kindError + return k12 where kindError = "kinds don't match in type application: " ++ show t ++ "\n" ++ @@ -533,39 +512,89 @@ checkTy es@(tcenv,tvenv) t = ch t ch (Tforall tb t) = do tvenv' <- extendTvenv tvenv tb - k <- checkTy (tcenv,tvenv') t - return $ case k of - -- distribute the forall - Keq t1 t2 -> Keq (Tforall tb t1) (Tforall tb t2) - _ -> k + checkTy (tcenv,tvenv') t ch (TransCoercion t1 t2) = do - k1 <- checkTy es t1 - k2 <- checkTy es t2 - case (k1, k2) of - (Keq ty1 ty2, Keq ty3 ty4) | ty2 == ty3 -> - return $ Keq ty1 ty4 - _ -> fail ("Bad kinds in trans. coercion: " ++ - show k1 ++ " " ++ show k2) + (ty1,ty2) <- checkTyCo es t1 + (ty3,ty4) <- checkTyCo es t2 + require (ty2 == ty3) ("Types don't match in trans. coercion: " ++ + show ty2 ++ " and " ++ show ty3) + return $ Keq ty1 ty4 ch (SymCoercion t1) = do - k <- checkTy es t1 - case k of - Keq ty1 ty2 -> return $ Keq ty2 ty1 - _ -> fail ("Bad kind in sym. coercion: " - ++ show k) + (ty1,ty2) <- checkTyCo es t1 + return $ Keq ty2 ty1 ch (UnsafeCoercion t1 t2) = do checkTy es t1 checkTy es t2 return $ Keq t1 t2 ch (LeftCoercion t1) = do - k <- checkTy es t1 + k <- checkTyCo es t1 case k of - Keq (Tapp u _) (Tapp w _) -> return $ Keq u w + ((Tapp u _), (Tapp w _)) -> return $ Keq u w _ -> fail ("Bad coercion kind in operand of left: " ++ show k) ch (RightCoercion t1) = do - k <- checkTy es t1 + k <- checkTyCo es t1 case k of - Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x + ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x _ -> fail ("Bad coercion kind in operand of left: " ++ show k) + ch (InstCoercion ty arg) = do + forallK <- checkTyCo es ty + case forallK of + ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do + require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: " + ++ show ty) + argK <- checkTy es arg + require (argK `eqKind` k1) ("Kind mismatch in type being " + ++ "instantiated: " ++ show arg) + let newLhs = substl [v1] [arg] b1 + let newRhs = substl [v2] [arg] b2 + return $ Keq newLhs newRhs + _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty) + +checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty) +checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = + (case splitTyConApp_maybe t of + Just (tc, tys) -> do + tcK <- qlookupM tcenv_ tcenv eempty tc + case tcK of + -- todo: avoid duplicating this code + -- blah, this almost calls for a different syntactic form + -- (for a defined-coercion app): (TCoercionApp Tcon [Ty]) + Coercion (DefinedCoercion tbs (from, to)) -> do + require (length tys == length tbs) $ + ("Arity mismatch in coercion app: " ++ show t) + let (tvs, tks) = unzip tbs + argKs <- mapM (checkTy es) tys + let kPairs = zip argKs tks + let kindsOk = all (uncurry eqKind) kPairs + if not kindsOk && + all (uncurry subKindOf) kPairs + -- see comments in checkTy about this + then warn $ "Applying coercion " ++ show tc ++ + " to arguments of kind " ++ show argKs + ++ " when it expects: " ++ show tks + else require kindsOk + ("Kind mismatch in coercion app: " ++ show tks + ++ " and " ++ show argKs ++ " t = " ++ show t) + return (substl tvs tys from, substl tvs tys to) + _ -> checkTapp t1 t2 + _ -> checkTapp t1 t2) + where checkTapp t1 t2 = do + (lhsRator, rhsRator) <- checkTyCo es t1 + (lhs, rhs) <- checkTyCo es t2 + -- Comp rule from paper + checkTy es (Tapp lhsRator lhs) + checkTy es (Tapp rhsRator rhs) + return (Tapp lhsRator lhs, Tapp rhsRator rhs) +checkTyCo (tcenv, tvenv) (Tforall tb t) = do + tvenv' <- extendTvenv tvenv tb + (t1,t2) <- checkTyCo (tcenv, tvenv') t + return (Tforall tb t1, Tforall tb t2) +checkTyCo es t = do + k <- checkTy es t + case k of + Keq t1 t2 -> return (t1, t2) + -- otherwise, expand by the "refl" rule + _ -> return (t, t) {- Type equality modulo newtype synonyms. -} equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool @@ -598,6 +627,10 @@ equalTy tsenv t1 t2 = expand (RightCoercion t1) = do exp1 <- expand t1 return $ RightCoercion exp1 + expand (InstCoercion t1 t2) = do + exp1 <- expand t1 + exp2 <- expand t2 + return $ InstCoercion exp1 exp2 expapp (t@(Tcon (m,tc))) ts = do env <- mlookupM tsenv_ tsenv eempty m case elookup env tc of @@ -685,6 +718,7 @@ substl tvs ts t = f (zip tvs ts) t UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2) LeftCoercion t1 -> LeftCoercion (f env t1) RightCoercion t1 -> RightCoercion (f env t1) + InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2) where free = foldr union [] (map (freeTvars.snd) env) t' = freshTvar free @@ -692,13 +726,14 @@ substl tvs ts t = f (zip tvs ts) t freeTvars :: Ty -> [Tvar] freeTvars (Tcon _) = [] freeTvars (Tvar v) = [v] -freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2) +freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1) freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 freeTvars (SymCoercion t) = freeTvars t freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 freeTvars (LeftCoercion t) = freeTvars t freeTvars (RightCoercion t) = freeTvars t +freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 {- Return any tvar *not* in the argument list. -} freshTvar :: [Tvar] -> Tvar diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs index 5f8ed82..66270cd 100644 --- a/utils/ext-core/Core.hs +++ b/utils/ext-core/Core.hs @@ -60,6 +60,7 @@ data Ty | TransCoercion Ty Ty | SymCoercion Ty | UnsafeCoercion Ty Ty + | InstCoercion Ty Ty | LeftCoercion Ty | RightCoercion Ty @@ -132,9 +133,9 @@ eqKind Kunlifted Kunlifted = True eqKind Kopen Kopen = True eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1 && k2 `eqKind` l2 -eqKind _ _ = False -- no Keq kind is ever equal to any other... - -- maybe ok for now? - +eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1 + && t2 == u2 +eqKind _ _ = False splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty]) splitTyConApp_maybe (Tvar _) = Nothing diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs index f080093..42e21e9 100644 --- a/utils/ext-core/ParsecParser.hs +++ b/utils/ext-core/ParsecParser.hs @@ -109,21 +109,6 @@ coreQualifiedGen p = (try (do -- unqualified name (p >>= (\ res -> return (Nothing, res))) -{- -coreMaybeMname = optionMaybe coreMname - -coreRequiredQualifiedName = do - mname <- coreMname - theId <- identifier - return (Just mname, theId) - -coreMname = do - char '^' - nm <- try coreModuleName - symbol "." - return nm --} - coreAxiom :: Parser Axiom coreAxiom = parens (do coercionName <- coreQualifiedCon @@ -204,7 +189,8 @@ coreBty = do Sym k -> app k 1 maybeRest "sym" Unsafe k -> app k 2 maybeRest "unsafe" LeftCo k -> app k 1 maybeRest "left" - RightCo k -> app k 1 maybeRest "right") + RightCo k -> app k 1 maybeRest "right" + InstCo k -> app k 2 maybeRest "inst") where app k arity args _ | length args == arity = k args app _ _ args err = primCoercionError (err ++ @@ -235,24 +221,26 @@ coreTcon = -- the "try"s are crucial; they force -- backtracking maybeCoercion <- choice [try symCo, try transCo, try unsafeCo, - try leftCo, rightCo] + try instCo, try leftCo, rightCo] return $ case maybeCoercion of TransC -> Trans (\ [x,y] -> TransCoercion x y) SymC -> Sym (\ [x] -> SymCoercion x) UnsafeC -> Unsafe (\ [x,y] -> UnsafeCoercion x y) LeftC -> LeftCo (\ [x] -> LeftCoercion x) - RightC -> RightCo (\ [x] -> RightCoercion x)) + RightC -> RightCo (\ [x] -> RightCoercion x) + InstC -> InstCo (\ [x,y] -> InstCoercion x y)) <|> (coreQualifiedCon >>= (return . ATy . Tcon)) -data CoercionTy = TransC | SymC | UnsafeC | LeftC | RightC +data CoercionTy = TransC | InstC | SymC | UnsafeC | LeftC | RightC -symCo, transCo, unsafeCo :: Parser CoercionTy +symCo, transCo, unsafeCo, instCo, leftCo, rightCo :: Parser CoercionTy -- Would be better not to wire these in quite this way. Sigh symCo = string "ghczmprim:GHCziPrim.sym" >> return SymC transCo = string "ghczmprim:GHCziPrim.trans" >> return TransC unsafeCo = string "ghczmprim:GHCziPrim.CoUnsafe" >> return UnsafeC leftCo = string "ghczmprim:GHCziPrim.left" >> return LeftC rightCo = string "ghczmprim:GHCziPrim.right" >> return RightC +instCo = string "ghczmprim:GHCziPrim.inst" >> return InstC coreForallTy :: Parser Ty coreForallTy = do @@ -270,7 +258,9 @@ coreKind = do return $ foldl Karrow hd maybeRest coreAtomicKind = try liftedKind <|> try unliftedKind - <|> try openKind {- <|> try (parens equalityKind) -} + <|> try openKind <|> try (do + (from,to) <- parens equalityKind + return $ Keq from to) <|> try (parens coreKind) liftedKind = do @@ -301,6 +291,7 @@ data ATyOp = | Unsafe ([Ty] -> Ty) | LeftCo ([Ty] -> Ty) | RightCo ([Ty] -> Ty) + | InstCo ([Ty] -> Ty) coreVdefGroups :: Parser [Vdefg] coreVdefGroups = option [] (do @@ -461,12 +452,15 @@ intOrRatLit :: Parser CoreLit intOrRatLit = do -- Int and lit combined into one to avoid ambiguity. -- Argh.... - lhs <- anIntLit + lhs <- intLit maybeRhs <- optionMaybe (symbol "%" >> anIntLit) case maybeRhs of Nothing -> return $ Lint lhs Just rhs -> return $ Lrational (lhs % rhs) +intLit :: Parser Integer +intLit = anIntLit <|> parens anIntLit + anIntLit :: Parser Integer anIntLit = do sign <- option 1 (symbol "-" >> return (-1)) diff --git a/utils/ext-core/Prep.hs b/utils/ext-core/Prep.hs index 05250af..df664a5 100644 --- a/utils/ext-core/Prep.hs +++ b/utils/ext-core/Prep.hs @@ -20,11 +20,6 @@ import Check import Data.List -primArgTys :: Env Var [Ty] -primArgTys = efromlist (map f (etolist (venv_ primEnv))) - where f (v,t) = (v,atys) - where (_,atys,_) = splitTy t - prepModule :: Menv -> Module -> Module prepModule globalEnv (Module mn tdefs vdefgs) = Module mn tdefs vdefgs' @@ -76,24 +71,38 @@ prepModule globalEnv (Module mn tdefs vdefgs) = unwindApp env (App e1 e2) as = unwindApp env e1 (Left e2:as) unwindApp env (Appt e t) as = unwindApp env e (Right t:as) unwindApp env (op@(Dcon qdc)) as = - etaExpand (drop n atys) (rewindApp env op as) + -- possibly dubious to assume no type args + etaExpand [] (drop n atys) (rewindApp env op as) where (tbs,atys0,_) = splitTy (qlookup cenv_ eempty qdc) atys = map (substl (map fst tbs) ts) atys0 ts = [t | Right t <- as] n = length [e | Left e <- as] unwindApp env (op@(Var(qv@(_,p)))) as | isPrimVar qv = - etaExpand (drop n atys) (rewindApp env op as) - where Just atys = elookup primArgTys p + etaExpand (snd (unzip extraTbs)) (drop n atys) (rewindApp env op as) + where -- TODO: avoid copying code. these two cases are the same + + -- etaExpand needs to add the type arguments too! Bah! + (tbs, atys0, _) = (maybe (error "unwindApp") splitTy (elookup (venv_ primEnv) p)) + n_args = length ts + (appliedTbs, extraTbs) = (take n_args tbs, drop n_args tbs) + atys = map (substl (map fst appliedTbs) ts) atys0 + ts = [t | Right t <- as] n = length [e | Left e <- as] unwindApp env op as = rewindApp env op as - etaExpand :: [Ty] -> Exp -> Exp - etaExpand ts e = - let args = [('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in - foldr (\ (v,t) e -> Lam (Vb (v,t)) e) - (foldl (\ e (v,_) -> App e (Var (unqual v))) e args) - args + etaExpand :: [Kind] -> [Ty] -> Exp -> Exp + etaExpand ks ts e = + -- what a pain + let tyArgs = [("$t_"++(show i),k) | (i, k) <- zip [(1::Integer)..] ks] + termArgs = [ ('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in + foldr (\ (t1,k1) e -> Lam (Tb (t1,k1)) e) + (foldr (\ (v,t) e -> Lam (Vb (v,t)) e) + (foldl (\ e (v,_) -> App e (Var (unqual v))) + (foldl (\ e (tv,_) -> Appt e (Tvar tv)) + e tyArgs) + termArgs) termArgs) + tyArgs rewindApp _ e [] = e rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindOfTy tvenv t `eqKind` Kunlifted && suspends e2 = diff --git a/utils/ext-core/PrimCoercions.hs b/utils/ext-core/PrimCoercions.hs index 7536cb6..8dd0176 100644 --- a/utils/ext-core/PrimCoercions.hs +++ b/utils/ext-core/PrimCoercions.hs @@ -11,12 +11,14 @@ pvz :: Id -> Qual Id pvz = (qual primMname) . (++ "zh") {- Coercions -} -symCoercion, transCoercion, unsafeCoercion :: Qual Tcon +symCoercion, transCoercion, unsafeCoercion, + leftCoercion, rightCoercion, instCoercion :: Qual Tcon symCoercion = pv "sym" transCoercion = pv "trans" unsafeCoercion = pv "CoUnsafe" leftCoercion = pv "left" -rightCoercion = pv "right" +rightCoercion = pv "right" +instCoercion = pv "inst" {- Addrzh -} tcAddrzh = pvz "Addr" diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs index 0cd8b09..2649a00 100644 --- a/utils/ext-core/Printer.hs +++ b/utils/ext-core/Printer.hs @@ -143,6 +143,8 @@ pty (LeftCoercion t) = (pqname leftCoercion <+> paty t) pty (RightCoercion t) = (pqname rightCoercion <+> paty t) +pty (InstCoercion t1 t2) = + (sep [pqname instCoercion, paty t1, paty t2]) pty t = pbty t pappty (Tapp t1 t2) ts = pappty t1 (t2:ts) diff --git a/utils/ext-core/README b/utils/ext-core/README index 9afd388..4fb16ff 100644 --- a/utils/ext-core/README +++ b/utils/ext-core/README @@ -9,15 +9,20 @@ tjc April 2008: ==== Notes ==== The checker should work on most programs. Bugs I'm aware of: -1. GHC generates some questionable coercion applications involving - partially-applied function arrows (for details, see: +1. There's some business I don't quite understand involving + coercions and subkinding (for details, see: http://www.haskell.org/pipermail/cvs-ghc/2008-April/041949.html) This shows up when typechecking a few of the library modules. - + 2. There's some weirdness involving funny character literals. This can be fixed by writing a new lexer for chars rather than using Parsec's built-in charLiteral lexer. But I haven't done that. +3. When typechecking the ghc-prim:GHC.PrimopWrappers library module, + some declarations seem to have the wrong type signature (due to + confusion between (forall (t::*) ...) and (forall (t::?) ...).) + This may be a GHC bug. + Typechecking all the GHC libraries eats about a gig of heap and takes a long time. I blame Parsec. (Someone who was bored, or understood happy better than I do, could update the old happy parser, which is still in the