Skip to content

Commit

Permalink
Specially type lists for better error messages
Browse files Browse the repository at this point in the history
  • Loading branch information
@twitu
twitu committed Sep 11, 2023
1 parent 92b2566 commit 25d752d
Show file tree
Hide file tree
Showing 13 changed files with 6,974 additions and 3,874 deletions.
19 changes: 19 additions & 0 deletions shared/src/main/scala/hmloc/Typer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -372,6 +372,25 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool)
val param_ty = typePattern(pat)(newCtx, raise, vars)
val body_ty = typeTerm(body)(newCtx, raise, vars)
FunctionType(param_ty, body_ty)(tp(term.toLoc, "function"))
// specialize Cons Nil application for better error messages
case cons@App(Var("Cons"), Tup(v :: Var("Nil") :: Nil)) =>
// version 2 inline Nil
// val arg_var = freshVar(tp(v.toCoveringLoc, "cons arg"))
// val v_ty = typeTerm(v)
// con(v_ty, arg_var, arg_var)
// TypeRef(TypeName("list"), arg_var :: Nil)(tp(cons.toLoc, "cons"))
// version 2 remove Nil completely
val v_ty = typeTerm(v)
TypeRef(TypeName("list"), v_ty :: Nil)(tp(cons.toLoc, "cons"))
// specialize Cons application for better error messages
case cons@App(Var("Cons"), Tup(v :: vs :: Nil)) =>
// version 2 simplified style
val arg_var = freshVar(tp(v.toCoveringLoc, "cons arg"))
val v_ty = typeTerm(v)
con(v_ty, arg_var, arg_var)
val vs_ty = typeTerm(vs)
val res_ty = TypeRef(TypeName("list"), v_ty :: Nil)(tp(cons.toLoc, "cons"))
con(vs_ty, res_ty, res_ty)
case App(f, a) =>
// version 2 simplified style
val fun_ty = typeTerm(f)
Expand Down
105 changes: 13 additions & 92 deletions shared/src/test/diff/ocaml/Jonathan.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -221,9 +221,9 @@ let rec additivePersistence n =
//│ additivePersistence: 'a -> 'b
//│ where
//│ 'b = bool, int
//│ U max: 6, total: 56
//│ U max: 4, total: 50
//│ UERR 1 errors
//│ L: 0 [bool ~ int, bool <: α121', α121' <: α111', α111' :> int]
//│ L: 0 [bool ~ int, bool <: α115', α115' <: α105', α105' :> int]

// The unification chain terminates at a higher level
// because int is a direct parameter of the list
Expand All @@ -233,52 +233,7 @@ let y x = [x]
let k a = if a then [2] else y true
//│ [ERROR] Type `bool` does not match `int`
//│
//│ (bool) ---> (?c) ~~~~ (?a0) ~~~~ (?a) ~~~~ (int)
//│
//│ ◉ (bool) comes from
//│ │ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^
//│ ▼
//│ ◉ (?c) is assumed for
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?c * _ list) comes from
//│ │ - l.1 let y x = [x]
//│ │ ^
//│ ▼
//│ ◉ (?a0 * ?a0 list) comes from
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?a0) is assumed for
//│ ◉ (?a0 list) comes from
//│ │ - l.1 let y x = [x]
//│ │ ^^^
//│ │ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^
//│ │ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ▼
//│ ◉ (?b) is assumed for
//│ ▲ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ │
//│ ◉ (?a list) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^^^
//│ ◉ (?a) is assumed for
//│ ◉ (?a * ?a list) comes from
//│ ▲ - l.2 let k a = if a then [2] else y true
//│ │ ^
//│ │
//│ ◉ (int * _ list) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^
//│ ◉ (int) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^
//│ [ERROR] Type `bool` does not match `int`
//│
//│ (bool) ---> (?b) ~~~~ (?a1) ~~~~ (?a) ~~~~ (?a1) ~~~~ (?a0) ~~~~ (int)
//│ (bool) ---> (?b) ~~~~ (int)
//│
//│ ◉ (bool) comes from
//│ │ - l.2 let k a = if a then [2] else y true
Expand All @@ -287,63 +242,29 @@ let k a = if a then [2] else y true
//│ ◉ (?b) is assumed for
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?b * ?a list) comes from
//│ │ - l.1 let y x = [x]
//│ │ ^
//│ ▼
//│ ◉ (?a1 * ?a1 list) comes from
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?a1) is assumed for
//│ ◉ (?a1 list) comes from
//│ ◉ (?a1 * ?a1 list) comes from
//│ ▲ - l.1 let y x = [x]
//│ │ ^
//│ │
//│ ◉ (?b * ?a list) comes from
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?a list) comes from
//│ ◉ (?a) is assumed for
//│ ◉ (?a list) comes from
//│ ◉ (?b * ?a list) comes from
//│ │ - l.1 let y x = [x]
//│ │ ^
//│ ▼
//│ ◉ (?a1 * ?a1 list) comes from
//│ - l.1 let y x = [x]
//│ ^
//│ ◉ (?a1 list) comes from
//│ ◉ (?a1) is assumed for
//│ ◉ (?a1 list) comes from
//│ ◉ (?b list) comes from
//│ │ - l.1 let y x = [x]
//│ │ ^^^
//│ │ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^
//│ │ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ▼
//│ ◉ (?c) is assumed for
//│ ◉ (?a) is assumed for
//│ ▲ - l.2 let k a = if a then [2] else y true
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^
//│ │
//│ ◉ (?a0 list) comes from
//│ ◉ (int list) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^^^
//│ ◉ (?a0) is assumed for
//│ ◉ (?a0 * ?a0 list) comes from
//│ ▲ - l.2 let k a = if a then [2] else y true
//│ │ ^
//│ │
//│ ◉ (int * _ list) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^
//│ ◉ (int) comes from
//│ - l.2 let k a = if a then [2] else y true
//│ ^
//│ y: 'a -> list['a]
//│ k: bool -> list[bool]
//│ U max: 5, total: 31
//│ UERR 2 errors
//│ L: 1 [bool ~ int, bool <: α132', [α132' - ([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],) - 'a133', L: 0 [([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],), ([[α132']], [[list['a134']]],) <: ('a133', list['a133'],)]], ['a133' - list['a133'] ~ list['a130'] - 'a130', L: 0 [list['a133'] ~ list['a130'], list['a133'] <: α129', α129' :> list['a130']]], ['a130' - ('a130', list['a130'],) ~ ([[int]], [[list['a131']]],) - int, L: 0 [('a130', list['a130'],) ~ ([[int]], [[list['a131']]],), ('a130', list['a130'],) :> ([[int]], [[list['a131']]],)]]]
//│ L: 2 [bool ~ int, bool <: α132', [α132' - ([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],) - 'a133', L: 0 [([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],), ([[α132']], [[list['a134']]],) <: ('a133', list['a133'],)]], ['a133' - list['a133'] ~ list['a134'] - 'a134', L: 1 [list['a133'] ~ list['a134'], [list['a133'] - ('a133', list['a133'],) ~ ([[α132']], [[list['a134']]],) - list['a134'], L: 0 [('a133', list['a133'],) ~ ([[α132']], [[list['a134']]],), ('a133', list['a133'],) :> ([[α132']], [[list['a134']]],)]]]], ['a134' - list['a134'] ~ list['a133'] - 'a133', L: 1 [list['a134'] ~ list['a133'], [list['a134'] - ([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],) - list['a133'], L: 0 [([[α132']], [[list['a134']]],) ~ ('a133', list['a133'],), ([[α132']], [[list['a134']]],) <: ('a133', list['a133'],)]]]], ['a133' - list['a133'] ~ list['a130'] - 'a130', L: 0 [list['a133'] ~ list['a130'], list['a133'] <: α129', α129' :> list['a130']]], ['a130' - ('a130', list['a130'],) ~ ([[int]], [[list['a131']]],) - int, L: 0 [('a130', list['a130'],) ~ ([[int]], [[list['a131']]],), ('a130', list['a130'],) :> ([[int]], [[list['a131']]],)]]]
//│ k: bool -> 'a
//│ where
//│ 'a = list['b], list[int]
//│ 'b = int, bool
//│ U max: 1, total: 7
//│ UERR 1 errors
//│ L: 1 [bool ~ int, bool <: α121', [α121' - list[[α121']] ~ list[[int]] - int, L: 0 [list[[α121']] ~ list[[int]], list[[α121']] <: α120', α120' :> list[[int]]]]]
Loading

0 comments on commit 25d752d

Please sign in to comment.