diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2016-02-15 15:50:24 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2016-02-15 16:21:52 +0000 |
| commit | 005712527af6c68c9fa9681d1f4ade5abd9ece88 (patch) | |
| tree | 72b01dfb646b0a1ea724859fd4c31b80ebf7f2a7 | |
| parent | f6b98ea75d56e479248643d413676a13f357b705 (diff) | |
| download | haskell-005712527af6c68c9fa9681d1f4ade5abd9ece88.tar.gz | |
Comments and white space
| -rw-r--r-- | compiler/coreSyn/CoreLint.hs | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index f094415a8f..6f199ea4f6 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1231,6 +1231,11 @@ lintStarCoercion g lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role) -- Check the kind of a coercion term, returning the kind -- Post-condition: the returned OutTypes are lint-free +-- +-- If lintCorecion co = (k1, k2, s1, s2, r) +-- then co :: s1 ~r s2 +-- s1 :: k2 +-- s2 :: k2 -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] @@ -1266,7 +1271,7 @@ lintCoercion co@(AppCo co1 co2) | Refl _ (TyConApp {}) <- co1 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co) | otherwise - = do { (k1,k2,s1,s2,r1) <- lintCoercion co1 + = do { (k1, k2, s1, s2, r1) <- lintCoercion co1 ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2 ; k3 <- lint_co_app co k1 [(t1,k'1)] ; k4 <- lint_co_app co k2 [(t2,k'2)] @@ -1448,7 +1453,7 @@ lintCoercion co@(AxiomInstCo con ind cos) (empty_subst, empty_subst) (zip3 (ktvs ++ cvs) roles cos) ; let lhs' = substTys subst_l lhs - rhs' = substTy subst_r rhs + rhs' = substTy subst_r rhs ; case checkAxInstCo co of Just bad_branch -> bad_ax $ text "inconsistent with" <+> pprCoAxBranch con bad_branch |