diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
| commit | 4eb93836d04d18f43d8c4360f290a7977d96c468 (patch) | |
| tree | ef38476a5b0199272d5dc20a65a306b4c7b2a112 /src/elab_err.sml | |
| parent | 37cf82d0761088c469205b90e35569674707202f (diff) | |
Add a new scoping check for unification variables, to fix a type inference bug
Diffstat (limited to 'src/elab_err.sml')
| -rw-r--r-- | src/elab_err.sml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml index 84c8c61f..2bf059e6 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -63,6 +63,7 @@ fun kindError env err = datatype kunify_error = KOccursCheckFailed of kind * kind | KIncompatible of kind * kind + | KScope of kind * kind fun kunifyError env err = case err of @@ -74,7 +75,10 @@ fun kunifyError env err = eprefaces "Incompatible kinds" [("Kind 1", p_kind env k1), ("Kind 2", p_kind env k2)] - + | KScope (k1, k2) => + eprefaces "Scoping prevents kind unification" + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)] fun p_con env c = P.p_con env (simplCon env c) @@ -122,6 +126,7 @@ datatype cunify_error = | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of con * con | TooDeep + | CScope of con * con fun cunifyError env err = case err of @@ -167,6 +172,10 @@ fun cunifyError env err = eprefaces' [("Replacement", p_con env c1), ("Body", p_con env c2)]) | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting" + | CScope (c1, c2) => + eprefaces "Scoping prevents constructor unification" + [("Have", p_con env c1), + ("Need", p_con env c2)] datatype exp_error = UnboundExp of ErrorMsg.span * string |