diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-09-18 13:51:13 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-09-18 13:51:13 -0400 |
| commit | 2a7c54badfcd4e30105a0127b25975000ff09bbb (patch) | |
| tree | fb5689a478c7dfd47263881e70c603199c3a6f71 /src/elab_err.sml | |
| parent | 39cf1b0633fd95ff82815741c9c3d35a0f762cf2 (diff) | |
Disallow wildcards in signatures (should help with #174)
Diffstat (limited to 'src/elab_err.sml')
| -rw-r--r-- | src/elab_err.sml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml index 385caca3..bbe1c160 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -40,11 +40,14 @@ val p_kind = P.p_kind datatype kind_error = UnboundKind of ErrorMsg.span * string + | KDisallowedWildcard of ErrorMsg.span fun kindError env err = case err of UnboundKind (loc, s) => ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) + | KDisallowedWildcard loc => + ErrorMsg.errorAt loc "Wildcard not allowed in signature" datatype kunify_error = KOccursCheckFailed of kind * kind @@ -76,6 +79,7 @@ datatype con_error = | DuplicateField of ErrorMsg.span * string | ProjBounds of con * int | ProjMismatch of con * kind + | CDisallowedWildcard of ErrorMsg.span fun conError env err = case err of @@ -101,6 +105,8 @@ fun conError env err = (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; eprefaces' [("Constructor", p_con env c), ("Kind", p_kind env k)]) + | CDisallowedWildcard loc => + ErrorMsg.errorAt loc "Wildcard not allowed in signature" datatype cunify_error = CKind of kind * kind * E.env * kunify_error |