Many updates and improvements to diagnostic messages #195
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Consider the following program:
structure S :
sig
type ('a, 'b) t
eqtype ('a, 'b) u
type 'a v = ('a, 'a) t * 'a * ('a, 'a) t
type 'a w = ('a, 'a) u * 'a * ('a, 'a) u
datatype 'a x = X of ('a, 'a) t
datatype 'a y = Y of ('a, 'a) u
end = struct end
Previously, MLton generated the following error messages:
Error: z.sml 2.1-9.3.
Type in signature but not in structure: t.
signature: type ('a, 'b) t = ('a, 'b) _sig.t
spec at: z.sml 3.18-3.18
Error: z.sml 2.1-9.3.
Type in signature but not in structure: u.
signature: eqtype ('a, 'b) u = ('a, 'b) _sig.u
spec at: z.sml 4.20-4.20
Error: z.sml 2.1-9.3.
Type in signature but not in structure: v.
signature: type 'a v = ('a, 'a) _sig.t * 'a * ('a, 'a) _sig.t
spec at: z.sml 5.12-5.12
Error: z.sml 2.1-9.3.
Type in signature but not in structure: w.
signature: eqtype 'a w = ('a, 'a) _sig.u * 'a * ('a, 'a) _sig.u
spec at: z.sml 6.12-6.12
Error: z.sml 2.1-9.3.
Type in signature but not in structure: x.
signature: datatype 'a x = X of ('a, 'a) _sig.t
spec at: z.sml 7.16-7.16
Error: z.sml 2.1-9.3.
Type in signature but not in structure: y.
signature: datatype 'a y = Y of ('a, 'a) _sig.u
spec at: z.sml 8.16-8.16
Note that the first two error messages are rather vacuous, asserting
that a type specified in the signature is equal to itself, while the
fourth error message asserts "eqtype", although the specification in
the signature is a realized "type".
Now, MLton generates the following error messages:
Error: z.sml 2.1-9.3.
Type in signature but not in structure: t.
signature: type ('b, 'a) t
spec at: z.sml 3.18-3.18
Error: z.sml 2.1-9.3.
Type in signature but not in structure: u.
signature: eqtype ('b, 'a) u
spec at: z.sml 4.20-4.20
Error: z.sml 2.1-9.3.
Type in signature but not in structure: v.
signature: type 'a v = ('a, 'a) _sig.t * 'a * ('a, 'a) _sig.t
spec at: z.sml 5.12-5.12
Error: z.sml 2.1-9.3.
Type in signature but not in structure: w.
signature: type 'a w = ('a, 'a) _sig.u * 'a * ('a, 'a) _sig.u
spec at: z.sml 6.12-6.12
Error: z.sml 2.1-9.3.
Type in signature but not in structure: x.
signature: datatype 'a x = X of ('a, 'a) _sig.t
spec at: z.sml 7.16-7.16
Error: z.sml 2.1-9.3.
Type in signature but not in structure: y.
signature: datatype 'a y = Y of ('a, 'a) _sig.u
spec at: z.sml 8.16-8.16
When there are elaboration errors, the compilation is effectively 'elaborateOnly'.
Due to the expansion of `e1 andalso e2` into `if e1 then false else e2`, the elaborated type of an `andalso` expression is taken to be the elaborated type of `e2`, even if `e2` is known not to be of type bool. Similarly, the elaborated type of `e: ty` is the elaborated type of `e`, even if `e` is known not to be of type `ty`. In these cases, force the type of the elaborated expression to be `bool` or `ty`, respectively, which can reduce spurious subsequent errors.
In a `val rec` declaration that binds multiple variables (in a correct program, such variables must be (nested) layered patterns), all AST variables must be mapped to the same CoreML variable, as only one variable is bound in the CoreML program. The `regression/valrec.sml` program triggered the bug.
Use `Avar.region` of the variable, rather then the region of the declaration.
In `<spec> sharing <longtycon1> = <longtycon2>`, the `<longtycon1>`
and `<longtycon2>` should be found in the environment of `<spec>`;
i.e., they should not be found in the outer environment in which the
`<spec> sharping <longtycon1> = <longtycon2>` is elaborated.
Consider the following program:
signature A =
sig
type a
sharing type a = unit
end
signature B =
sig
type b
structure C:
sig
type c
sharing type c = b
end
end
signature T = sig type t end
structure D: T =
struct
type t = unit
end
signature E =
sig
structure F: T
sharing F = D
end
signature G =
sig
structure H: T
structure I:
sig
structure J: T
sharing H = J
end
end
Previously, MLton generated the following error messages:
Error: z.sml 4.21-4.24.
Type unit is a definition and cannot be shared.
Error: z.sml 13.27-13.27.
Type b is not local and cannot be shared.
Error: z.sml 27.15-27.15.
Undefined structure: D.
Error: z.sml 36.17-36.17.
Type H.t is not local and cannot be shared.
This correctly rejects the program, but (arguably) for the wrong
reasons.
Now, MLton generates the following error messages:
Error: z.sml 4.21-4.24.
Undefined type unit.
Error: z.sml 13.27-13.27.
Undefined type b.
Error: z.sml 27.15-27.15.
Undefined structure D.
Error: z.sml 36.17-36.17.
Undefined structure H.
which better corresponds to a scoping error.
Consider the following program:
structure Z:
sig
type ('a, 'b, 'c) t
end =
struct
type 'a t = unit
end
Previously, MLton generated the following error message:
Error: z.sml 2.1-4.3.
Type in structure disagrees with signature (arity): t.
structure: type ['a] t = ...
defn at: z.sml 6.12-6.12
signature: type [('a, 'c, 'b)] t
spec at: z.sml 3.22-3.22
Note that type variables in the signature specification are not in
alphabetical order, owing to the fact that `Vector.toListMap`
traverses the vector from right to left when forcing the pretty names
of the type variables.
Now, MLton generates the following error message:
Error: z.sml 2.1-4.3.
Type in structure disagrees with signature (arity): t.
structure: type ['a] t = ...
defn at: z.sml 6.12-6.12
signature: type [('a, 'b, 'c)] t
spec at: z.sml 3.22-3.22
Consider the following program:
signature S =
sig
type s1
type s2 = int
sharing type s1 = s2
end
signature S =
sig
type s1
type s2 = s1 * s1
sharing type s1 = s2
end
signature S =
sig
structure T: sig type t end
structure U:
sig
type u1 = T.t
type u2
sharing type u1 = u2
end
end
signature S =
sig
structure T: sig datatype t = T1 end
structure U: sig type 'a u end
structure V: sig eqtype ('a, 'b) v end
sharing type T.t = U.u = V.v
end
signature S =
sig
type s = int
end where type s = bool
signature S =
sig
type s1
type s2 = s1 * s1
end where type s2 = bool
signature S =
sig
type t
end where type 'a t = 'a -> 'a
signature S =
sig
eqtype t
end where type t = unit -> unit
signature S =
sig
eqtype 'a t
end where type ('a, 'b) t = 'a -> 'b
signature S =
sig
datatype t = T
end where type 'a t = 'a -> 'a
Previously, MLton generated the following error messages:
Error: z.sml 5.22-5.23.
Type s2 is already defined as int and cannot be shared.
Error: z.sml 12.22-12.23.
Type s2 is a definition and cannot be shared.
Error: z.sml 22.23-22.24.
Type u1 is not local and cannot be shared.
Error: z.sml 31.4-31.31.
Type T.t has arity 0 and type U.u has arity 1 and cannot be shared.
Error: z.sml 31.4-31.31.
Type U.u has arity 1 and type V.v has arity 2 and cannot be shared.
Error: z.sml 37.5-37.23.
Type s is already defined as int and cannot be redefined.
Error: z.sml 43.5-43.24.
Type s2 is a definition and cannot be redefined.
Error: z.sml 48.5-48.30.
Type t has arity 0 and cannot be defined to have arity 1.
Error: z.sml 53.5-53.31.
Eqtype t cannot be defined as a non-equality type.
Error: z.sml 58.5-58.36.
Type t has arity 1 and cannot be defined to have arity 2.
Error: z.sml 63.5-63.30.
Type t has arity 0 and cannot be defined to have arity 1.
Now, MLton generates the following error messages:
Error: z.sml 5.22-5.23.
Type cannot be shared (defined): s2.
type spec: type s2 = [...]
spec at: z.sml 4.9-4.10
Error: z.sml 12.22-12.23.
Type cannot be shared (defined): s2.
type spec: type s2 = [...]
spec at: z.sml 11.9-11.10
Error: z.sml 22.23-22.24.
Type cannot be shared (not local): u1.
type spec: type u1
spec at: z.sml 20.15-20.16
Error: z.sml 31.4-31.31.
Types cannot be shared (arity): T.t, U.u.
type spec: datatype [] T.t = ...
spec at: z.sml 28.30-28.30
type spec: type ['a] U.u
spec at: z.sml 29.29-29.29
Error: z.sml 31.4-31.31.
Types cannot be shared (arity): U.u, V.v.
type spec: type ['a] U.u
spec at: z.sml 29.29-29.29
type spec: eqtype [('b, 'a)] V.v
spec at: z.sml 30.37-30.37
Error: z.sml 37.16-37.16.
Type cannot be realized (defined): s.
type spec: type s = [...]
spec at: z.sml 36.9-36.9
Error: z.sml 43.16-43.17.
Type cannot be realized (defined): s2.
type spec: type s2 = [...]
spec at: z.sml 42.9-42.10
Error: z.sml 48.5-48.30.
Type cannot be realized (arity): t.
type spec: type [] t
spec at: z.sml 47.9-47.9
type defn: <arity 1>
Error: z.sml 53.5-53.31.
Type cannot be realized (admits equality): t.
type spec: [eqtype] t
spec at: z.sml 52.11-52.11
type defn: <non-equality>
Error: z.sml 58.5-58.36.
Type cannot be realized (arity, admits equality): t.
type spec: [eqtype] ['a] t
spec at: z.sml 57.14-57.14
type defn: <arity 2>, <non-equality>
Error: z.sml 63.5-63.30.
Type cannot be realized (arity, admits equality, type structure): t.
type spec: [datatype] [] t = ...
spec at: z.sml 62.13-62.13
type defn: <arity 1>, <non-equality>, <complex type>
Previously, when creating a type structure from a scheme that was an eta-expansion of a type constructor, the type structure was recorded as a Tycon, rather than as a Scheme. But, this makes it difficult to determine if the specification was abstract (`type t`) or a definition (`type t = int`). Shift the eta-check to Interface.TypeStr.toTyconOpt.
Rather than using `exn` for unknown types, gensym a bogus type. Also, when a type constructor is applied to the wrong number of type arguments, either take from or add to the given types to obtain the right number of type arguments. In particular, this preserves the type constructor.
When a type constructor is applied to the wrong number of type arguments, either take from or add to the given types to obtain the right number of type arguments. In particular, this preserves the type constructor.
Like 5d0158f. Previously, when creating a type structure from a scheme that was an eta-expansion of a type constructor, the type structure was recorded as a Tycon, rather than as a Scheme. Shift the eta-check to Interface.TypeStr.toTyconOpt.
Share the infrastructure for extending an environment.
Consider the following program:
datatype a = A
signature T =
sig
type a = a
type b
type c
type d
type t = a * b * c * d -> unit
end
signature S =
sig
type a
type c
structure T1:
sig
structure T2 :
sig
include T where type b = a
where type d = c
end
end where type T2.t = unit
structure T3:
sig
structure T4 :
sig
include T where type b = a
where type d = c
end
end
structure T5:
sig
structure T6 :
sig
include T where type b = a
where type d = c
end
end
sharing type T3.T4.t = T5.T6.t
end
Previously, MLton generated the following error messages:
Error: z.sml 21.25-21.28.
Type cannot be realized (defined): T2.t.
type spec: type T2.t = a * _sig.a * _sig.T1.T2.c * _sig.c -> unit
spec at: z.sml 8.12-8.12
Error: z.sml 38.20-38.26.
Type cannot be shared (defined): T3.T4.t.
type spec: type T3.T4.t = a * _sig.a * _sig.T3.T4.c * _sig.c -> unit
spec at: z.sml 8.12-8.12
Error: z.sml 38.30-38.36.
Type cannot be shared (defined): T5.T6.t.
type spec: type T5.T6.t = a * _sig.a * _sig.T5.T6.c * _sig.c -> unit
spec at: z.sml 8.12-8.12
Although the use of "_sig" could be explained as "the top-level
signature being elaborated", it can still be confusing when shadowed
type constructors are not displayed with "?." prefixes.
Now, MLton generates the following error messages:
Error: z.sml 21.25-21.28.
Type cannot be realized (defined): T2.t.
type spec: type T2.t = ?.a * a * _sig.T2.c * c -> unit
spec at: z.sml 8.12-8.12
Error: z.sml 38.20-38.26.
Type cannot be shared (defined): T3.T4.t.
type spec: type T3.T4.t = ?.a * a * T3.T4.c * c -> unit
spec at: z.sml 8.12-8.12
Error: z.sml 38.30-38.36.
Type cannot be shared (defined): T5.T6.t.
type spec: type T5.T6.t = ?.a * a * T5.T6.c * c -> unit
spec at: z.sml 8.12-8.12
Now, the displayed type definition is relative to the environment at
the error point. For "where type" signatures, a "_sig." prefix is
used for flexible type constructors that only exist in the signature
being realized; the contents of that signature are not in scope at the
error point, hence the "_sig." prefix.
Consider the following program:
datatype ('a, 'b) w = W of 'a -> 'b
datatype x = X
datatype y = Y of unit -> unit
signature S =
sig
structure T1: sig type t end
structure T2: sig datatype t = T end
sharing type T1.t = T2.t
structure T3: sig type t end
structure T4: sig eqtype t end
sharing type T3.t = T4.t
eqtype 'a u
datatype 'a v = V of 'a
structure X1: sig datatype x = X end where type x = x
structure X2: sig datatype x = datatype x end
end where type 'a T1.t = unit -> unit
where type 'a T2.t = unit -> unit
where type T3.t = y
where type T4.t = y
where type u = unit -> unit
where type ('a, 'b) v = ('a, 'b) w
where type X1.x = unit
where type X2.x = unit
Previously, MLton generated the following error messages
Error: z.sml 16.8-16.40.
Type cannot be realized (arity, admits equality, type structure): T1.t.
type spec: [eqtype] [] T1.t
spec at: z.sml 6.30-6.30
spec at: z.sml 8.7-8.30
type defn: <arity 1>, <non-equality>, <complex type>
Error: z.sml 17.8-17.40.
Type cannot be realized (arity, admits equality, type structure): T2.t.
type spec: [datatype] [] T2.t = ...
spec at: z.sml 7.34-7.34
spec at: z.sml 8.7-8.30
type defn: <arity 1>, <non-equality>, <complex type>
Error: z.sml 18.8-18.26.
Type cannot be realized (admits equality): T3.t.
type spec: [eqtype] T3.t
spec at: z.sml 9.30-9.30
spec at: z.sml 11.7-11.30
type defn: <non-equality>
Error: z.sml 19.8-19.26.
Type cannot be realized (admits equality): T4.t.
type spec: [eqtype] T4.t
spec at: z.sml 10.32-10.32
spec at: z.sml 11.7-11.30
type defn: <non-equality>
Error: z.sml 20.8-20.34.
Type cannot be realized (arity, admits equality): u.
type spec: [eqtype] ['a] u
spec at: z.sml 12.17-12.17
type defn: <arity 0>, <non-equality>
Error: z.sml 21.8-21.41.
Type cannot be realized (arity, admits equality): v.
type spec: [datatype] ['a] v = ...
spec at: z.sml 13.19-13.19
type defn: <arity 2>, <non-equality>
Error: z.sml 22.19-22.22.
Type cannot be realized (defined): X1.x.
type spec: type X1.x = x
spec at: z.sml 14.34-14.34
spec at: z.sml 14.44-14.59
Error: z.sml 23.19-23.22.
Type cannot be realized (defined): X2.x.
type spec: type X2.x = x
spec at: z.sml 15.34-15.34
Now, MLton generates the following error messages:
Error: z.sml 16.8-16.40.
Type cannot be realized (arity, type structure): T1.t.
type spec: type [] T1.t = [_sig.T2.t]
spec at: z.sml 6.30-6.30
spec at: z.sml 8.7-8.30
type defn: type ['a] T1.t = [unit -> unit]
Error: z.sml 17.8-17.40.
Type cannot be realized (arity, type structure): T2.t.
type spec: [datatype] [] T2.t = ...
spec at: z.sml 7.34-7.34
spec at: z.sml 8.7-8.30
type defn: type ['a] T2.t = [unit -> unit]
Error: z.sml 18.8-18.26.
Type cannot be realized (admits equality): T3.t.
type spec: type T3.t = [_sig.T4.t]
spec at: z.sml 9.30-9.30
spec at: z.sml 11.7-11.30
type defn: type T3.t = [y]
Error: z.sml 19.8-19.26.
Type cannot be realized (admits equality): T4.t.
type spec: [eqtype] T4.t
spec at: z.sml 10.32-10.32
spec at: z.sml 11.7-11.30
type defn: type T4.t = [y]
Error: z.sml 20.8-20.34.
Type cannot be realized (arity, admits equality): u.
type spec: [eqtype] ['a] u
spec at: z.sml 12.17-12.17
type defn: type [] u = [unit -> unit]
Error: z.sml 21.8-21.41.
Type cannot be realized (arity, admits equality): v.
type spec: datatype ['a] v = ...
spec at: z.sml 13.19-13.19
type defn: type [('a, 'b)] v = [('a, 'b) w]
Error: z.sml 22.19-22.22.
Type cannot be realized (defined): X1.x.
type spec: datatype X1.x = ... (* = datatype x *)
spec at: z.sml 14.34-14.34
spec at: z.sml 14.44-14.59
Error: z.sml 23.19-23.22.
Type cannot be realized (defined): X2.x.
type spec: datatype X2.x = ... (* = datatype x *)
spec at: z.sml 15.34-15.34
The schemes registered for def-use information are not always true
schemes. For example, consider the following program:
fun f (x: 'a) (y: 'b) =
let
fun g (z: 'c) = (z, y, x)
in
g ()
end
The "scheme" registered for `f` and `g` are actually mono-types: the
unification types created for `f` and `g` at the point where they are
initially added to the environment. During inference, these
unification types are unfied with function type and, at
generalization, the remaining unification types are replaced by type
variables. Hence, the "scheme" that remains for `f` and `g` are the
mono-types with free type variables. (Similarly, the "scheme"
registered for `x`, `y`, and `z` are mono-types with free type
variables.)
To yield reasonable def-use extra information, these "schemes" are
pretty-printed with fresh local names for each distinct type
variable. This makes each scheme look reasonable in isolation, but the
total information is not globally consistent. For example, the
def-use information for the above program is:
variable f z.sml 2.5 "'a -> 'b -> unit * 'b * 'a"
variable x z.sml 2.8 "'a"
z.sml 4.30
variable y z.sml 2.16 "'a"
z.sml 4.27
variable g z.sml 4.11 "'a -> 'a * 'b * 'c"
z.sml 6.7
variable z z.sml 4.14 "'a"
z.sml 4.24
Note that each of `x`, `y`, and `z` reports the type `'a`, despite the
fact that they must be distinct type variables.
This is probably better than the previous behavior (on this
branch) which would fall-thru to the default `Tyvar.layout` (with
gen-sym names):
variable f z.sml 2.5 "'a_0 -> 'b_0 -> unit * 'b_0 * 'a_0"
variable x z.sml 2.8 "'a_0"
z.sml 4.30
variable y z.sml 2.16 "'b_0"
z.sml 4.27
variable g z.sml 4.11 "'c_0 -> 'c_0 * 'b_0 * 'a_0"
z.sml 6.7
variable z z.sml 4.14 "'c_0"
z.sml 4.24
While this information is globally consistent, in a full program,
with many inferred type variables, most polymorphic values have
schemes with `'a_2342`-style type variables, which are difficult
to read.
"Pretty" and "globally consistent" information would require some
effort. In any case, this restores the (master branch) behavior
of `-keep-def-use`.
Clarify that only flexible tycons can have equality status changed.
In very rare circumstances, a flexible tycon may be referenced (and
displayed in a diagnostic) but not in scope (and not have a pretty
name set). For example, consider the following program:
datatype a = A
signature T =
sig
type a = a
type b
type c
type d
type t = a * b * c * d -> unit
end
signature S =
sig
type a
type c
structure T1:
sig
structure T2 :
sig
type a
include T where type b = a
where type d = c
end
end where type T2.t = unit
end
Previously, MLton generated the error messages:
Error: z.sml 19.27-20.44.
Duplicate type specification: a.
spec at: z.sml 18.24-18.24
spec at: z.sml 4.12-4.12
Error: z.sml 22.25-22.28.
Type cannot be realized (defined): T2.t.
type spec: type T2.t = ?.a
* ?.{admitsEquality = Never,
creationTime = 132,
hasCons = false,
id = 9238,
kind = 0}
* _sig.T2.c
* c
-> unit
spec at: z.sml 8.12-8.12
At the `where type T2.t = unit`, the `type a` of `T2` has been shadowed
by the `include T`, although the flexible tycon `b` of `T` has been
realized as the shadowed `a`.
Now, MLton generates the following error messages:
Error: z.sml 19.27-20.44.
Duplicate type specification: a.
spec at: z.sml 18.24-18.24
spec at: z.sml 4.12-4.12
Error: z.sml 22.25-22.28.
Type cannot be realized (defined): T2.t.
type spec: type T2.t = ?.a * ??.a * _sig.T2.c * c -> unit
spec at: z.sml 8.12-8.12
Like shadowed tycons, a shadowed flexible tycon is displayed with a
default name (the name of the AST tycon that introduced it) prefixed
with "??".
Consider the following program:
structure A =
struct
datatype a = A
structure B =
struct
datatype b = B
end
val b = B.B
structure B = struct end
val _ : unit = b
end
signature T =
sig
type a = A.a
type b
type c
type d
type t = a * b * c * d -> unit
end
structure A = struct end
signature S =
sig
type a
type c
structure T1:
sig
structure T2 :
sig
type a
include T where type b = a
where type d = c
end
end where type T2.t = unit
end
Now, MLton generates the following error messages:
Error: z.sml 10.11-10.22.
Pattern and expression disagree.
pattern: [unit]
expression: [?.A.B.b]
in: val _: unit = b
Error: z.sml 30.27-31.44.
Duplicate type specification: a.
spec at: z.sml 29.24-29.24
spec at: z.sml 14.12-14.12
Error: z.sml 33.25-33.28.
Type cannot be realized (defined): T2.t.
type spec: type T2.t = ?.A.a * ??.S.T1.T2.a * _sig.T2.c * c -> unit
spec at: z.sml 18.12-18.12
Note in the first error message that the default pretty name for a
shadowed tycon includes the structure in which it is being defined.
Now, in the last error message, the default pretty name for a flexible
tycon includes the signature in which it is being defined.
Previously, the last error message had "??.a" instead of
"??.S.T1.T2.a".
Consider the following program:
signature T =
sig
type u
type t
end
signature S =
sig
type u
include T where type t = u -> u
end
structure S: S =
struct
type u = unit
type t = u -> u
end
functor F (S: S): S = struct open S end
Previously, MLton generated an ICE:
Error: z.sml 9.15-9.37.
Duplicate type specification: u.
spec at: z.sml 8.12-8.12
spec at: z.sml 3.12-3.12
unhandled exception: Fail: Interface.FlexibleTycon.realization
This occurs at the `structure S: S = ...` matching (and would occur
again at the creation of the dummy structure for the functor argument
and again at the "functor F (S: S): S = ...` result matching. The
issue is that the shadowed `type u` in `signature S` is a flexible
tycon, but because it is shadowed, it is not reported as a flexible
tycon nor is it realized. Nonetheless, the `type t` is realized as
`u -> u` for the shadowed `u`, which requires obtaining the
realization of the shadowed `u` to check the realized type of `t`.
Now, MLton generates the following error messages:
Error: z.sml 9.15-9.37.
Duplicate type specification: u.
spec at: z.sml 8.12-8.12
spec at: z.sml 3.12-3.12
Error: z.sml 11.14-11.14.
Type in structure disagrees with signature (type definition): t.
structure: type t = [unit] -> [unit]
defn at: z.sml 14.12-14.12
signature: type t = [?.??.S.u] -> [?.??.S.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 9.17-9.37
Error: z.sml 16.19-16.19.
Type in structure disagrees with signature (type definition): t.
structure: type t = [?.??.S.u] -> [?.??.S.u]
defn at: z.sml 4.12-4.12
signature: type t = [?.??.S.u] -> [?.??.S.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 9.17-9.37
It is difficult to give a good pretty name for this realization of a
shadowed flexible tycon, but it is also a rather obscure kind of error
and the "?.??." prefix seems to convey the difficulty.
Consider the following program:
signature T =
sig
type u
type t
end
signature S =
sig
type u
include T where type t = u -> u
end where type t = unit
structure S:
sig
type u
include T where type t = u -> u
end =
struct
type u = unit
type t = u -> u
end
functor F (type u
include T where type t = u -> u):
sig
type u
include T where type t = u -> u
end =
struct
type u = u
type t = t
end
functor G (X: sig
type u
include T where type t = u -> u
end):
sig
type u
include T where type t = u -> u
end =
struct
open X
end
Now, MLton generates the following error messages:
Error: z.sml 9.15-9.37.
Duplicate type specification: u.
spec at: z.sml 8.12-8.12
spec at: z.sml 3.12-3.12
Error: z.sml 10.19-10.19.
Type cannot be realized (defined): t.
type spec: type t = ??.S.u -> ??.S.u
spec at: z.sml 4.12-4.12
spec at: z.sml 9.17-9.37
Error: z.sml 14.15-14.37.
Duplicate type specification: u.
spec at: z.sml 13.12-13.12
spec at: z.sml 3.12-3.12
Error: z.sml 12.4-15.6.
Type in structure disagrees with signature (type definition): t.
structure: type t = [unit] -> [unit]
defn at: z.sml 18.12-18.12
signature: type t = [?.??._sig.u] -> [?.??._sig.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 14.17-14.37
Error: z.sml 21.20-21.42.
Duplicate type specification: u.
spec at: z.sml 20.17-20.17
spec at: z.sml 3.12-3.12
Error: z.sml 24.15-24.37.
Duplicate type specification: u.
spec at: z.sml 23.12-23.12
spec at: z.sml 3.12-3.12
Error: z.sml 22.4-25.6.
Type in structure disagrees with signature (type definition): t.
structure: type t = [?.??._argF.u] -> [?.??._argF.u]
defn at: z.sml 28.12-28.12
signature: type t = [?.??._sig.u] -> [?.??._sig.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 24.17-24.37
Error: z.sml 32.26-32.48.
Duplicate type specification: u.
spec at: z.sml 31.23-31.23
spec at: z.sml 3.12-3.12
Error: z.sml 36.15-36.37.
Duplicate type specification: u.
spec at: z.sml 35.12-35.12
spec at: z.sml 3.12-3.12
Error: z.sml 34.4-37.6.
Type in structure disagrees with signature (type definition): t.
structure: type t = [?.??._argG.u] -> [?.??._argG.u]
defn at: z.sml 4.12-4.12
signature: type t = [?.??._sig.u] -> [?.??._sig.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 36.17-36.37
Consider the following program:
signature T = sig eqtype t end
signature S = T where type t = (unit -> unit) * unit
structure S: T = struct type t = (unit -> unit) * unit end
Previously, MLton generated the following error messages:
Error: z.sml 2.17-2.52.
Type cannot be realized (admits equality): t.
type spec: [eqtype] t
spec at: z.sml 1.26-1.26
type defn: type t = [(unit -> unit) * unit]
Error: z.sml 3.14-3.14.
Type in structure disagrees with signature (admits equality): t.
structure: type t = [_ -> _] * _
defn at: z.sml 3.30-3.30
signature: [eqtype] t
spec at: z.sml 1.26-1.26
Note the different treatment of the non-equality type in "type cannot
be realized" and "type in structure disagrees with signature".
Now, MLton generates the following error messages:
Error: z.sml 2.17-2.52.
Type cannot be realized (admits equality): t.
type spec: [eqtype] t
spec at: z.sml 1.26-1.26
type defn: type t = [_ -> _] * _
Error: z.sml 3.14-3.14.
Type in structure disagrees with signature (admits equality): t.
structure: type t = [_ -> _] * _
defn at: z.sml 3.30-3.30
signature: [eqtype] t
spec at: z.sml 1.26-1.26
Consider the following program:
signature S =
sig
eqtype u
type t
sharing type t = u
end where type t = unit -> unit
Previously, MLton generated the following error message:
Error: z.sml 6.8-6.34.
Type cannot be realized (admits equality): t.
type spec: type t = [_sig.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 5.7-5.24
type defn: type t = [_ -> _]
The specs include the "type t" and the "sharing type t = u", but not
the "eqtype t" which establishes the equality typeness.
Now, MLton generates the following error message:
Error: z.sml 6.8-6.34.
Type cannot be realized (admits equality): t.
type spec: type t = [_sig.u]
spec at: z.sml 4.12-4.12
spec at: z.sml 3.14-3.14
spec at: z.sml 5.7-5.24
type defn: type t = [_ -> _]
Consider the following program:
val id: 'a -> 'a = fn x => x
val f: 'a -> 'a = id id
val g = id (fn (x: 'a) => x)
val _ = (f 1, f true)
Previously, MLton generated the following diagnostics:
Error: z.sml 2.5-2.5.
Type of variable cannot be generalized in expansive declaration: f.
type: ['a] -> ['a]
in: val 'a f: ('a -> 'a) = id id
Error: z.sml 3.5-3.5.
Type of variable cannot be generalized in expansive declaration: g.
type: ['a] -> ['a]
in: val 'a g = id (fn x: 'a => x)
Error: z.sml 5.15-5.20.
Function applied to incorrect argument.
expects: [int]
but got: [bool]
in: f true
Warning: z.sml 3.5-3.5.
Type of variable was not inferred and could not be generalized: g.
type: ??? -> ???
in: val 'a g = id (fn x: 'a => x)
Taking the type annotation on `f` as the user's intention, the
subsequent type error at the application `f true` is spurious.
Now, MLton generates the following diagnostics:
Error: z.sml 2.5-2.5.
Type of variable cannot be generalized in expansive declaration: f.
type: ['a] -> ['a]
in: val 'a f: ('a -> 'a) = id id
Error: z.sml 3.5-3.5.
Type of variable cannot be generalized in expansive declaration: g.
type: ['a] -> ['a]
in: val 'a g = id (fn x: 'a => x)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Highlights:
compilation-error-regexp-alistto support full regions andspec at: <region>,defn at: <region>,escape from: <region>,escape to: <region>,scoped to: <region>informative messages (f4ceafb, f94f6ec, 2be2a29, 76bf730, 2be2a29, 44125b0).allow{Redefine,Specify}SpecialIdsexpert MLB annotations (a69b4b3), allowitto be defined/specified (87f6e6e), and treat=as a special identifier (d754ac9).funandval recdeclarations (4e3ca55, 007bd77, 0a9ab61, 4ea1f7c, 92ee067). The primary motivation is avoid the (confusing)recursive use of function disagrees with its typeerror message; in particular, it can be frustrating to add type constraints to a declaration in the hopes of identifying the problematic recursive use, only to have the explicit type information seemingly ignored. For example, consider the program:<thing> in structure disagrees with signaturediagnostic corresponds to the signature constraint, in order to fix the error, at least one of the structure or signature must be modified. Newdefn at: <region>andspec at: <region>informative messages are added to<thing> in structure disagrees with signaturediagnostics to identify the definition and specification points of the identifier. With suitable editor support (e.g., emacscompilation-error-regexp-alist), it is easy to visit one of the points to resolve the error. For example, consider the program:sharing typespecifications andwhere typesignature expressions (80170ac, dccddcf, e570564, 3224c6e, 054ef37, 12e494e, a9a3508, 6803627, 084003d). The newspec at: <region>informative messages show the origin and constraints of type constructors equated bysharing typeandwhere type. For example, consider the following program:escaping from: <region>andescaping to: <region>informative messages show the definition point of escaping type constructors and the declaration region of unification variables being unified. For example, consider the program:-show-basis <file>display of information (a14c363, a95aabd).structure S1 = S2 = S3 = ... = Sn(f2e88a4, 9cb5164, 198f585).exnorunit(48f0f79); make "time" of tyvars and tycons immutable and eliminateuseBeforeDefcomponent ofTypeEnv.Time.t(a4d81f2, c5db99b, 39541ee, 11c32be, 422e379, a9ace8d, b72ee8d, 87cde1f); properly separate AST Tyvar from Elaborate/CoreML Tyvar (76e59c4); simplify type variable scope inference (fb516c6, 34cfb55); eliminatepreErrorfrom elaboration (a3d96c9); simplifyElaborateEnv.Equalitytype and operations (2cdfe15); close a space leak withTypeEnv.Type.newCloses(6893e89); alternative implementation ofTypeEnv.close(d8fb739); refactorElaborateEnv(d1a850c, 24b5308, 3d5fffe, 465de43, 6bdcc14, 844d421). The general theme has been to eliminate or reduce the use of mutation.Overall, no significant impact on performance (when self-compiling)::