%% %% CoreLint.ott %% %% defines formal version of core typing rules %% %% See accompanying README file %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Static semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% defns CoreLint :: '' ::= defn |- prog program :: :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{GHC/Core/Lint.hs}{lintCoreBindings} }} {{ tex \labeledjudge{prog} [[program]] }} by G = no_duplicates --------------------- :: CoreBindings |-prog defn G |- bind binding :: :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{GHC/Core/Lint.hs}{lint\_bind} }} {{ tex [[G]] \labeledjudge{bind} [[binding]] }} by G |-sbind n <- e ---------------------- :: NonRec G |-bind n = e |-sbind ni <- ei // i /> ---------------------- :: Rec G |-bind rec defn G |- sbind n <- e :: :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{GHC/Core/Lint.hs}{lintSingleBinding} }} {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }} by G; empty |-tm e : t G |-name z_t ok = fv(t) ----------------- :: SingleBinding G |-sbind z_t <- e defn G ; D |-sjbind l vars <- e : t :: :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{GHC/Core/Lint.hs}{lintSingleBinding} }} {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }} by = inits() G, ; D |-tm e : t G |-label p/I_s ok = fv(s) split_I s = t ----------------- :: SingleBinding G; D |-sjbind p/I_s <- e : t defn G ; D |- tm e : t :: :: lintCoreExpr :: 'Tm_' {{ com Expression typing, \coderef{GHC/Core/Lint.hs}{lintCoreExpr} }} {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }} by x_t elt G not (t is_a_coercion_type) ------------------ :: Var G; D |-tm x_t : t t = literalType lit ------------------- :: Lit G; D |-tm lit : t G; empty |-tm e : s G |-co g : s k1~Rep k2 t k2 elt { *, # } ------------------- :: Cast G; D |-tm e |> g : t G; empty |-tm e : t ------------------- :: Tick G; D |-tm e {tick} : t G' = G, alpha_k G |-ki k ok G' |-subst alpha_k |-> s ok G'; D |-tm e[alpha_k |-> s] : t --------------------------- :: LetTyKi G; D |-tm let alpha_k = s in e : t G |-sbind x_s <- u G |-ty s : k k = * \/ k = # G, x_s ; D |-tm e : t ------------------------- :: LetNonRec G; D |-tm let x_s = u in e : t = inits() no_duplicates G' = G, G'; D |-tm e : t ------------------------ :: LetRec G; D |-tm let rec in e : t G; D |-sjbind l <- u : t G; D, l |-tm e : t ------------------------------------------- :: JoinNonRec G; D |-tm join l = u in e : t no_duplicates D' = D, <- ui : t // i /> G; D' |-tm e : t ------------------------------------------------------------- :: JoinRec G; D |-tm join rec = ui // i /> in e : t % lintCoreArg is incorporated in these next two rules G; empty |-tm e : forall alpha_k.t G |-subst alpha_k |-> s ok ---------------- :: AppType G; D |-tm e s : t[alpha_k |-> s] not (e2 is_a_type) G; empty |-tm e1 : t1 -> t2 G; empty |-tm e2 : t1 ---------------- :: AppExpr G; D |-tm e1 e2 : t2 p/I_s elt D split_I s = t --------------------- :: Jump G; D |-tm jump p/I_s : t not (k is_a_coercion_type) G |-ty t : k G, x_t; |-tm e : s ----------------- :: LamId G; D |-tm \x_t.e : t -> s G |-ki k ok G,alpha_k; |-tm e : t --------------------------- :: LamTy G; D |-tm \alpha_k.e : forall alpha_k. t phi = s1 k1~#k2 s2 G |-ki phi ok G,c_phi; |-tm e : t -------------------------------- :: LamCo G; D |-tm \c_phi.e : forall c_phi.t G; empty |-tm e : s s = * \/ s = # G |-ty t : TYPE s2 ---------------------------------------------------- :: Case G; D |-tm case e as z_s return t of : t G |-co g : t1 k1~Nom k2 t2 -------------------- :: Coercion G; D |-tm g : t1 k1~#k2 t2 G |-co g : t1 k1~Rep k2 t2 ----------------------- :: CoercionRep G; D |-tm g : (~Rep#) k1 k2 t1 t2 defn G |- name n ok :: :: lintSingleBinding_lintBinder :: 'Name_' {{ com Name consistency check, \coderef{GHC/Core/Lint.hs}{lintSingleBinding\#lintBinder} }} {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }} by G |-ty t : k k = * \/ k = # ----------------- :: Id G |-name x_t ok ----------------- :: TyVar G |-name alpha_k ok defn G |- label l ok :: :: lintSingleBinding_lintBinder_join :: 'Label_' {{ com Label consistency check, \coderef{GHC/Core/Lint.hs}{lintSingleBinding\#lintBinder} }} {{ tex [[G]] \labeledjudge{label} [[l]] [[ok]] }} by G |- ty t : k k = * \/ k = # split_I t = t' G |- ty t' : k' k' = * \/ k' = # ----------------- :: Label G |-label p / I _ t ok defn G |- bnd n ok :: :: lintBinder :: 'Binding_' {{ com Binding consistency, \coderef{GHC/Core/Lint.hs}{lintBinder} }} {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }} by G |-ty t : k k = * \/ k = # --------------------------------- :: Id G |-bnd x_t ok G |-ki k ok ---------------------------------------- :: TyVar G |-bnd alpha_k ok defn G |- co g : t1 k1 ~ R k2 t2 :: :: lintCoercion :: 'Co_' {{ com Coercion typing, \coderef{GHC/Core/Lint.hs}{lintCoercion} }} {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{ {}^{[[k1]]} {\sim}_{[[R]]}^{[[k2]]} } [[t2]] }} by G |-ty t : k ---------------------- :: Refl G |-co : t k~Nom k t G |-ty t : k ---------------------- :: GReflMRefl G |-co R MRefl : t k~R k t G |-ty t : k1 G |-co g : k1 *~Nom * k2 ---------------------- :: GReflMCo G |-co R MCo g : t k1~R k2 (t |> g) G |-co g1 : s1 k1~R k'1 t1 G |-co g2 : s2 k2~R k'2 t2 G |-arrow k1 -> k2 : k G |-arrow k'1 -> k'2 : k' ------------------------- :: FunCo G |-co g1 ->_R g2 : (s1 -> s2) k~R k' (t1 -> t2) T /= (->) = take(length , tyConRolesX R T) G |-app : tyConKind T ~> k' G |-app : tyConKind T ~> k --------------------------------- :: TyConAppCo G |-co T_R : T k'~R k T G |-co g1 : s1 k1~R k2 s2 G |-co g2 : t1 k1'~Nom k2' t2 G |-app (t1 : k1') : k1 ~> k3 G |-app (t2 : k2') : k2 ~> k4 --------------------- :: AppCo G |-co g1 g2 : (s1 t1) k3~R k4 (s2 t2) G |-co g1 : s1 k1 ~Ph k2 s2 G |-co g2 : t1 k1' ~Ph k2' t2 G |-app (t1 : k1') : k1 ~> k3 G |-app (t2 : k2') : k2 ~> k4 --------------------- :: AppCoPhantom G |-co g1 g2 : (s1 t1) k3~Ph k4 (s2 t2) G |-co h : k1 *~Nom * k2 G, alpha_k1 |-co g : t1 k3~R k4 t2 ------------------------------------------------------------------ :: ForAllCo_Tv G |-co forall alpha:h. g : (forall alpha_k1. t1) k3~R k4 (forall alpha_k2. (t2[alpha |-> alpha_k2 |> sym h])) G |-co h : k1 *~Nom * k2 G, x_k1 |-co g : t1 {TYPE s1}~R {TYPE s2} t2 R2 = coercionRole x_k1 h' = downgradeRole R2 h h1 = nth R2 2 h' h2 = nth R2 3 h' almostDevoid x g ------------------------------------------- :: ForAllCo_Cv G |-co forall x:h.g : (forall x_k1. t1) *~R * (forall x_k2. (t2[ x |-> h1 ; x_k2 ; sym h2 ])) z_phi elt G phi = t1 k1~#k2 t2 ----------------------- :: CoVarCoNom G |-co z_phi : t1 k1 ~Nom k2 t2 z_phi elt G phi = t1 k1 ~Rep# k2 t2 --------------------- :: CoVarCoRepr G |-co z_phi : t1 k1 ~Rep k2 t2 G |-co h : k1 *~Nom * k2 G |-ty t1 : k1 G |-ty t2 : k2 (R <= Ph \/ not (classifiesTypeWithValues k1)) \\/ (not (classifiesTypeWithValues k2) \/ compatibleUnBoxedTys t1 t2) ------------------------------------------------------ :: UnivCoUnsafe G |-co UnsafeCoerceProv _R^(h) : t1 k1~R k2 t2 G |-co h : k1 *~Nom * k2 G |-ty t1 : k1 G |-ty t2 : k2 -------------------------------------------------- :: UnivCoPhantom G |-co PhantomProv _Ph^(h) : t1 k1~Ph k2 t2 G |-co h : phi1 *~Nom * phi2 G |-ty g1 : phi1 G |-ty g2 : phi2 -------------------------------------------------- :: UnivCoProofIrrel G |-co ProofIrrelProv _R^(h) : g1 phi1~R phi2 g2 G |-co g : t1 k1~R k2 t2 ------------------------- :: SymCo G |-co sym g : t2 k2~R k1 t1 G |-co g1 : t1 k1~R k2 t2 G |-co g2 : t2 k2~R k3 t3 ----------------------- :: TransCo G |-co g1 ; g2 : t1 k1~R k3 t3 G |-co g : (T ) k1~R k1' (T ) length = length i < length G |-ty si : k2 G |-ty ti : k2' not (si is_a_coercion) not (ti is_a_coercion) R' = (tyConRolesX R T)[i] ---------------------- :: NthCoTyCon G |-co nth R' i g : si k2~R' k2' ti G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2) --------------------------- :: NthCoForAll G |-co nth Nom 0 g : k1 *~Nom * k2 G |-co g : (s1 s2) k~Nom k' (t1 t2) G |-ty s1 : k1 G |-ty t1 : k1' ----------------------- :: LRCoLeft G |-co Left g : s1 k1~Nom k1' t1 G |-co g : (s1 s2) k~Nom k' (t1 t2) G |-ty s2 : k2 G |-ty t2 : k2' not (s2 is_a_coercion) not (t2 is_a_coercion) ----------------------- :: LRCoRight G |-co Right g : s2 k2~Nom k2' t2 G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2) G |-co h : s1 k1~Nom k2 s2 --------------------- :: InstCo G |-co g @ h : (t1[z1_k1 |-> s1]) k3~R k4 (t2[z2_k2 |-> s2]) C = T_R0 0 <= ind < length forall . ( ~> t1) = ()[ind] G |-axk [ |-> ] ~> (subst1, subst2) no_conflict(C, , ind, ind-1) t2 = subst2(t1) s2 = T G |-ty s2 : k G |-ty t2 : k' ------------------------------------------------------ :: AxiomInstCo G |-co C ind : s2 k~R0 k' t2 G |-co g : t1 k1~R k2 t2 -------------------------- :: KindCo G |-co kind g : k1 *~Nom * k2 G |-co g : s k' ~Nom k t ------------------------- :: SubCo G |-co sub g : s k' ~Rep k t mu = M(i, , R') Just (t'1, t'2) = coaxrProves mu G |-ty t'1 : k0 G |-ty t'2 : k0' --------------------------------------------------------------------- :: AxiomRuleCo G |-co mu $ : t'1 k0 ~R' k0' t'2 defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) :: :: check_ki :: 'AxiomKind_' {{ com Axiom argument kinding, \coderef{GHC/Core/Lint.hs}{lintCoercion\#check\_ki} }} {{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }} by --------------------------------------- :: Empty G |-axk [empty |-> empty] ~> (empty, empty) G |-axk [namesroles |-> gs] ~> (subst1, subst2) n = z_k G |-co g0 : t1 {subst1(k)}~R subst2(k) t2 ----------------------------- :: Arg G |-axk [ namesroles, n_R |-> gs, g0 ] ~> (subst1 [n |-> t1], subst2 [n |-> t2]) defn validRoles T :: :: checkValidRoles :: 'Cvr_' {{ com Type constructor role validity, \coderef{GHC/Tc/TyCl.hs}{checkValidRoles} }} by = tyConDataCons T = tyConRoles T Ki // i /> ------------------------------------ :: DataCons validRoles T defn validDcRoles K :: :: check_dc_roles :: 'Cdr_' {{ com Data constructor role validity, \coderef{GHC/Tc/TyCl.hs}{check\_dc\_roles} }} by forall . forall . $ -> T = dataConRepType K , |- tcc : Rep // cc /> --------------------------------- :: Args validDcRoles K defn O |- t : R :: :: check_ty_roles :: 'Ctr_' {{ com Type role validity, \coderef{GHC/Tc/TyCl.hs}{check\_ty\_roles} }} {{ tex [[O]] \labeledjudge{ctr} [[t]] : [[R]] }} by O(n) = R' R' <= R ---------- :: TyVarTy O |- n : R = tyConRoles T O |- ti : Ri // i /> -------------------------- :: TyConAppRep O |- T : Rep --------------------------- :: TyConAppNom O |- T : Nom O |- t1 : R O |- t2 : Nom -------------------------- :: AppTy O |- t1 t2 : R O |- t1 : R O |- t2 : R ------------------- :: FunTy O |- t1 -> t2 : R O, n : Nom |- t : R --------------------- :: ForAllTy O |- forall n. t : R ------------------ :: LitTy O |- lit : R O |- t : R --------------- :: CastTy O |- t |> g : R ------------ :: CoercionTy O |- g : Ph defn R1 <= R2 :: :: ltRole :: 'Rlt_' {{ com Sub-role relation, \coderef{GHC/Core/Coercion.hs}{ltRole} }} {{ tex [[R1]] \leq [[R2]] }} by -------- :: Nominal Nom <= R -------- :: Phantom R <= Ph ------- :: Refl R <= R defn G |- ki k ok :: :: lintKind :: 'K_' {{ com Kind validity, \coderef{GHC/Core/Lint.hs}{lintKind} }} {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }} by G |-ty k : * -------------- :: Star G |-ki k ok G |-ty k : # -------------- :: Hash G |-ki k ok defn G |- ty t : k :: :: lintType :: 'Ty_' {{ com Kinding, \coderef{GHC/Core/Lint.hs}{lintType} }} {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }} by z_k elt G ------------ :: TyVarTy G |-ty z_k : k G |-ty t1 : k1 G |-ty t2 : k2 G |-app (t2 : k2) : k1 ~> k --------------- :: AppTy G |-ty t1 t2 : k G |-ty t1 : k1 G |-ty t2 : k2 G |-arrow k1 -> k2 : k ------------------- :: FunTy G |-ty t1 -> t2 : k not (isUnLiftedTyCon T) \/ length = tyConArity T G |-app : tyConKind T ~> k --------------------------- :: TyConApp G |-ty T : k G |-ki k1 ok G, alpha_k1 |-ty t : TYPE s not (alpha elt fv(s)) ------------------------ :: ForAllTy_Tv G |-ty forall alpha_k1. t : TYPE s phi = s1 k1~#k2 s2 G |-ki phi ok G, x_phi |-ty t : TYPE s x elt fv(t) --------------------- :: ForAllTy_Cv G |-ty forall x_phi.t : * G |-tylit lit : k -------------- :: LitTy G |-ty lit : k G |-ty t : k1 G |-co g : k1 *~Nom * k2 --------------------- :: CastTy G |-ty t |> g : k2 G |-co g : t1 k1 ~Nom k2 t2 -------------- :: CoercionTy_Nom G |-ty g : t1 k1 ~# k2 t2 G |-co g : t1 k1 ~Rep k2 t2 ------------------- :: CoercionTy_Repr G |-ty g : (~Rep#) k1 k2 t1 t2 defn G |- subst n |-> t ok :: :: lintTyKind :: 'Subst_' {{ com Substitution consistency, \coderef{GHC/Core/Lint.hs}{lintTyKind} }} {{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }} by G |-ty t : k ---------------------- :: Type G |-subst z_k |-> t ok defn G ; D ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_' {{ com Case alternative consistency, \coderef{GHC/Core/Lint.hs}{lintCoreAlt} }} {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }} by G; D |-tm e : t --------------------- :: DEFAULT G; D; s |-altern _ -> e : t s = literalType lit G; D |-tm e : t ---------------------------------------- :: LitAlt G; D; s |-altern lit -> e : t T = dataConTyCon K not (isNewTyCon T) t1 = dataConRepType K t2 = t1 {} G' = G, G' |-altbnd : t2 ~> T G'; D |-tm e : t --------------------------------------- :: DataAlt G; D; T |-altern K -> e : t defn t' = t { } :: :: applyTys :: 'ApplyTys_' {{ com Telescope substitution, \coderef{GHC/Core/Type.hs}{applyTys} }} by --------------------- :: Empty t = t { } t' = t{} t'' = t'[n |-> s] -------------------------- :: Ty t'' = (forall n. t) { s, } defn G |- altbnd vars : t1 ~> t2 :: :: lintAltBinders :: 'AltBinders_' {{ com Case alternative binding consistency, \coderef{GHC/Core/Lint.hs}{lintAltBinders} }} {{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }} by ------------------------- :: Empty G |-altbnd empty : t ~> t G |-subst beta_k' |-> alpha_k ok G |-altbnd : t[beta_k' |-> alpha_k] ~> s ------------------------------------------------------ :: TyVar G |-altbnd alpha_k, : (forall beta_k'.t) ~> s G |-altbnd : t[z_phi |-> c_phi] ~> s ------------------------------------------------------- :: IdCoercion G |-altbnd c_phi, : (forall z_phi.t) ~> s G |-altbnd : t2 ~> s ----------------------------------------------- :: IdTerm G |-altbnd x_t1, : (t1 -> t2) ~> s defn G |- arrow k1 -> k2 : k :: :: lintArrow :: 'Arrow_' {{ com Arrow kinding, \coderef{GHC/Core/Lint.hs}{lintArrow} }} {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }} by k1 elt { *, # } k2 = TYPE s ------------------------- :: Kind G |-arrow k1 -> k2 : * defn G |- app kinded_types : k1 ~> k2 :: :: lint_app :: 'App_' {{ com Type application kinding, \coderef{GHC/Core/Lint.hs}{lint\_app} }} {{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }} by --------------------- :: Empty G |-app empty : k ~> k G |-app : k2 ~> k' ---------------------------------------------------- :: FunTy G |-app (t : k1), : (k1 -> k2) ~> k' G |-app : k2[z_k1 |-> t] ~> k' -------------------------------------------------------- :: ForAllTy G |-app (t : k1), : (forall z_k1. k2) ~> k' defn no_conflict ( C , , ind1 , ind2 ) :: :: check_no_conflict :: 'NoConflict_' {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{GHC/Core/Coercion/Opt.hs}{checkAxInstCo} \\ and \coderef{GHC/Core/FamInstEnv.hs}{compatibleBranches} } }} by ------------------------------------------------ :: NoBranch no_conflict(C, , ind, -1) C = T_R forall . ( ~> t') = ()[ind2] apart(, ) no_conflict(C, , ind1, ind2-1) ------------------------------------------------ :: Incompat no_conflict(C, , ind1, ind2) C = T_R forall . ( ~> s) = ()[ind1] forall . ( ~> s') = ()[ind2] apart(, ) no_conflict(C, , ind1, ind2-1) ------------------------------------------- :: CompatApart no_conflict(C, , ind1, ind2) C = T_R forall . ( ~> s) = ()[ind1] forall . ( ~> s') = ()[ind2] unify(, ) = subst subst(s) = subst(s') ----------------------------------------- :: CompatCoincident no_conflict(C, , ind1, ind2) defn |- axiom C ok :: :: lint_axiom :: 'Ax_' {{ com Coercion axiom linting, \coderef{GHC/Core/Lint.hs}{lint\_axiom} }} {{ tex \labeledjudge{axiom} [[C]] [[ok]] }} by isNewTyCon T = tyConRoles T |-ty T : k0 |-ty s : k0 ------------------------------ :: Newtype |-axiom T_Rep forall . ( ~> s) ok isOpenTypeFamilyTyCon T T |-branch b ok ------------------------------ :: OpenTypeFamily |-axiom T_Nom b ok isClosedTypeFamilyTyCon T --------------------------- :: ClosedTypeFamily |-axiom T_Nom ok isDataFamilyTyCon T T |-branch b ok --------------------------- :: DataFamily |-axiom T_Rep b ok defn T |- branch b ok :: :: lint_family_branch :: 'Br_' {{ com Type family branch linting, \coderef{GHC/Core/Lint.hs}{lint\_family\_branch} }} {{ tex [[T]] \labeledjudge{branch} [[b]] [[ok]] }} by fv() = |-ty T : k0 |-ty s : k0 ---------------------------------------------------------------- :: OK T |-branch forall . ( ~> s) ok