Skip to content

Commit

Permalink
Reduce type variables created
Browse files Browse the repository at this point in the history
  • Loading branch information
@twitu
twitu committed Nov 13, 2023
1 parent 25d752d commit 7b36b55
Show file tree
Hide file tree
Showing 9 changed files with 775 additions and 777 deletions.
2 changes: 0 additions & 2 deletions shared/src/main/scala/hmloc/Typer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,9 +385,7 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool)
// 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)
Expand Down
6 changes: 3 additions & 3 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: 4, total: 50
//│ U max: 4, total: 44
//│ UERR 1 errors
//│ L: 0 [bool ~ int, bool <: α115', α115' <: α105', α105' :> int]
//│ L: 0 [bool ~ int, bool <: α114', α114' <: α105', α105' :> int]

// The unification chain terminates at a higher level
// because int is a direct parameter of the list
Expand Down Expand Up @@ -267,4 +267,4 @@ let k a = if a then [2] else y true
//│ '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]]]]]
//│ L: 1 [bool ~ int, bool <: α120', [α120' - list[[α120']] ~ list[[int]] - int, L: 0 [list[[α120']] ~ list[[int]], list[[α120']] <: α119', α119' :> list[[int]]]]]
414 changes: 207 additions & 207 deletions shared/src/test/diff/ocaml/OcamlComparison.mls
View file

Large diffs are not rendered by default.

1,038 changes: 519 additions & 519 deletions shared/src/test/diff/ocaml/OcamlDataset.mls
View file

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions shared/src/test/diff/ocaml/OcamlExprChecker.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ type ('a, 'b) heapD = HeapD of 'a * 'b list
//│ res: list[(string, int,)]
//│ res: heap
//│ res: heap
//│ U max: 2, total: 6
//│ U max: 2, total: 5
//│ UERR 1 errors
//│ L: 0 [list[([[string]], [[int]],)] ~ heap, list[([[string]], [[int]],)] <: heap]

Expand Down Expand Up @@ -231,7 +231,7 @@ let interp2 = (fun (env:env) opt ->
//│ interp2: err -> int
//│ U max: 1, total: 2
//│ UERR 1 errors
//│ L: 0 [err ~ option['a99'], err <: option['a99']]
//│ L: 0 [err ~ option['a94'], err <: option['a94']]

let head xs = match xs with
Cons(x, xs) -> x
Expand Down Expand Up @@ -349,7 +349,7 @@ let checkagain (v: (int, int, (int, int))) =
//│ checkagain: (int, int, (int, int,),) -> int
//│ U max: 3, total: 15
//│ UERR 2 errors
//│ L: 2 [int ~ err, [int - ([int], [int],) ~ ([[err]], [[err]],) - err, L: 1 [([int], [int],) ~ ([[err]], [[err]],), [([int], [int],) - ([int], [int], [([int], [int],)],) ~ ([α124'], [α125'], [α126'],) - α126', L: 0 [([int], [int], [([int], [int],)],) ~ ([α124'], [α125'], [α126'],), ([int], [int], [([int], [int],)],) :> α122', α122' <: ([α124'], [α125'], [α126'],)]], α126' <: ([[err]], [[err]],)]]]
//│ L: 2 [int ~ err, [int - ([int], [int],) ~ ([[err]], [[err]],) - err, L: 1 [([int], [int],) ~ ([[err]], [[err]],), [([int], [int],) - ([int], [int], [([int], [int],)],) ~ ([α119'], [α120'], [α121'],) - α121', L: 0 [([int], [int], [([int], [int],)],) ~ ([α119'], [α120'], [α121'],), ([int], [int], [([int], [int],)],) :> α117', α117' <: ([α119'], [α120'], [α121'],)]], α121' <: ([[err]], [[err]],)]]]
//│ L: 0 [err ~ int, err <: int]

let (<): 'a -> 'a -> bool
Expand Down Expand Up @@ -416,7 +416,7 @@ let g x = x, if true then x else x
//│ - l.1 [0, 1; 2, 3, 4]
//│ ^^^^
//│ res: list[(int, int,)]
//│ U max: 1, total: 3
//│ U max: 1, total: 2
//│ UERR 1 errors
//│ L: 1 [([[int]], [[int]], [[int]],) ~ ([[int]], [[int]],), [([[int]], [[int]], [[int]],) - list[([[int]], [[int]], [[int]],)] ~ list[([[int]], [[int]],)] - ([[int]], [[int]],), L: 0 [list[([[int]], [[int]], [[int]],)] ~ list[([[int]], [[int]],)], list[([[int]], [[int]], [[int]],)] <: list[([[int]], [[int]],)]]]]

Expand Down Expand Up @@ -463,5 +463,5 @@ let len ls = match ls with | "hd :: tl" -> 1 | [] -> 0
//│ 'b = list['a], string
//│ U max: 1, total: 4
//│ UERR 1 errors
//│ L: 0 [string ~ list['a162'], string :> α160', α160' <: list['a162']]
//│ L: 0 [string ~ list['a154'], string :> α152', α152' <: list['a154']]

8 changes: 4 additions & 4 deletions shared/src/test/diff/ocaml/SurveyHard2.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,9 +103,9 @@ let bigAdd l1 l2 =
//│ ◉ (_ * _) comes from
//│ - l.14 let (_,res) = List.fold_left f base args in res in
//│ ^^^^^^^
//│ U max: 63, total: 468
//│ U max: 59, total: 448
//│ UERR 3 errors
//│ L: 2 [int ~ ([α127''], [α128''],), [int - (α123'' -> [int]) ~ (α121'' -> α120'') - α120'', L: 1 [(α123'' -> [int]) ~ (α121'' -> α120''), [(α123'' -> [int]) - (α122'' -> (α123'' -> [int])) ~ (α120'' -> (α121'' -> α120'')) - (α121'' -> α120''), L: 0 [(α122'' -> (α123'' -> [int])) ~ (α120'' -> (α121'' -> α120'')), (α122'' -> (α123'' -> [int])) <: (α120'' -> (α121'' -> α120''))]]]], α120'' <: ([α127''], [α128''],)]
//│ L: 1 [int ~ ([α127''], [α128''],), int :> α122'', [α122'' - (α122'' -> (α123'' -> [int])) ~ (α120'' -> (α121'' -> α120'')) - α120'', L: 0 [(α122'' -> (α123'' -> [int])) ~ (α120'' -> (α121'' -> α120'')), (α122'' -> (α123'' -> [int])) <: (α120'' -> (α121'' -> α120''))]], α120'' <: ([α127''], [α128''],)]
//│ L: 0 [int ~ ([α127''], [α128''],), int <: α120'', α120'' <: ([α127''], [α128''],)]
//│ L: 0 [int ~ ([α123''], [α124''],), int <: α116'', α116'' <: ([α123''], [α124''],)]
//│ L: 1 [int ~ ([α123''], [α124''],), int :> α118'', [α118'' - (α118'' -> (α119'' -> [int])) ~ (α116'' -> (α117'' -> α116'')) - α116'', L: 0 [(α118'' -> (α119'' -> [int])) ~ (α116'' -> (α117'' -> α116'')), (α118'' -> (α119'' -> [int])) <: (α116'' -> (α117'' -> α116''))]], α116'' <: ([α123''], [α124''],)]
//│ L: 2 [int ~ ([α123''], [α124''],), [int - (α119'' -> [int]) ~ (α117'' -> α116'') - α116'', L: 1 [(α119'' -> [int]) ~ (α117'' -> α116''), [(α119'' -> [int]) - (α118'' -> (α119'' -> [int])) ~ (α116'' -> (α117'' -> α116'')) - (α117'' -> α116''), L: 0 [(α118'' -> (α119'' -> [int])) ~ (α116'' -> (α117'' -> α116'')), (α118'' -> (α119'' -> [int])) <: (α116'' -> (α117'' -> α116''))]]]], α116'' <: ([α123''], [α124''],)]

64 changes: 32 additions & 32 deletions shared/src/test/diff/ocaml/SurveyHard3.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,19 +36,19 @@ let bigAdd l1 l2 =
(* List.rev: 'a list -> 'a list reverses a list *)
//│ [ERROR] Type `_ list` does not match `_ * _`
//│
//│ (_ list) ---> (?b) <--- (?a) ---> (_ * _)
//│ (_ list) ---> (?a) <--- (?b) ---> (_ * _)
//│
//│ ◉ (_ list) comes from
//│ │ - l.19 if x = []
//│ │ ^^
//│ ▼
//│ ◉ (?b) is assumed for
//│ ◉ (?a) is assumed for
//│ ▲ - l.19 if x = []
//│ │ ^
//│ │ - l.17 let f a x =
//│ │ ^
//│ │
//│ ◉ (?a) is assumed for
//│ ◉ (?b) is assumed for
//│ │ - l.17 let f a x =
//│ │ ^
//│ │ - l.22 (let (toSum1,toSum2) = x in
Expand All @@ -59,7 +59,7 @@ let bigAdd l1 l2 =
//│ ^^^^^^^^^^^^^^^
//│ [ERROR] Type `_ * _` does not match `_ list`
//│
//│ (_ * _) ~~~~ (?a) ~~~~ (?b) ~~~~ (?c) ---> (?d) <--- (_ list)
//│ (_ * _) ~~~~ (?c) ~~~~ (?d) ~~~~ (?a) ---> (?b) <--- (_ list)
//│
//│ ◉ (_ * _) comes from
//│ - lib. let List.combine: 'a list -> 'b list -> ('a * 'b) list
Expand All @@ -70,48 +70,48 @@ let bigAdd l1 l2 =
//│ │ - l.28 let args = List.rev (List.combine l1 l2) in
//│ │ ^^^^^^^^^^^^^^^^^^^^
//│ ▼
//│ ◉ (?a list) comes from
//│ ◉ (?c list) comes from
//│ - lib. let List.rev: 'a list -> 'a list
//│ ^^^^^^^
//│ ◉ (?a) is assumed for
//│ ◉ (?a list) comes from
//│ ◉ (?c) is assumed for
//│ ◉ (?c list) comes from
//│ │ - lib. let List.rev: 'a list -> 'a list
//│ │ ^^^^^^^
//│ │ - l.28 let args = List.rev (List.combine l1 l2) in
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ │ - l.29 let (_,res) = List.fold_left f base args in res in
//│ │ ^^^^
//│ ▼
//│ ◉ (?b list) comes from
//│ ◉ (?d list) comes from
//│ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ ^^^^^^^
//│ ◉ (?b) is assumed for
//│ ◉ (?b -> _) comes from
//│ ◉ (?d) is assumed for
//│ ◉ (?d -> _) comes from
//│ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ ^^^^^^^^
//│ ◉ (_ -> ?b -> _) comes from
//│ ◉ (_ -> ?d -> _) comes from
//│ ▲ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ │ ^^^^^^^^^^^^^^
//│ │ - l.29 let (_,res) = List.fold_left f base args in res in
//│ │ ^
//│ │
//│ ◉ (_ -> ?c -> _) comes from
//│ ◉ (_ -> ?a -> _) comes from
//│ - l.17 let f a x =
//│ ^^^^^
//│ let (carry,currentSum) = a in ...
//│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ◉ (?c -> _) comes from
//│ ◉ (?a -> _) comes from
//│ - l.17 let f a x =
//│ ^^^
//│ let (carry,currentSum) = a in ...
//│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ◉ (?c) is assumed for
//│ ◉ (?a) is assumed for
//│ │ - l.17 let f a x =
//│ │ ^
//│ │ - l.19 if x = []
//│ │ ^
//│ ▼
//│ ◉ (?d) is assumed for
//│ ◉ (?b) is assumed for
//│ ▲ - l.19 if x = []
//│ │ ^^
//│ │
Expand All @@ -120,59 +120,59 @@ let bigAdd l1 l2 =
//│ ^^
//│ [ERROR] Type `_ list` does not match `_ * _`
//│
//│ (_ list) ---> (?c) <--- (?b) ~~~~ (?a) ~~~~ (?b) ---> (_ * _)
//│ (_ list) ---> (?b) <--- (?a) ~~~~ (?c) ~~~~ (?a) ---> (_ * _)
//│
//│ ◉ (_ list) comes from
//│ │ - l.19 if x = []
//│ │ ^^
//│ ▼
//│ ◉ (?c) is assumed for
//│ ◉ (?b) is assumed for
//│ ▲ - l.19 if x = []
//│ │ ^
//│ │
//│ ◉ (?b) is assumed for
//│ ◉ (?a) is assumed for
//│ - l.17 let f a x =
//│ ^
//│ ◉ (?b -> _) comes from
//│ ◉ (?a -> _) comes from
//│ - l.17 let f a x =
//│ ^^^
//│ let (carry,currentSum) = a in ...
//│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ◉ (_ -> ?b -> _) comes from
//│ ◉ (_ -> ?a -> _) comes from
//│ │ - l.17 let f a x =
//│ │ ^^^^^
//│ │ let (carry,currentSum) = a in ...
//│ │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ │ - l.29 let (_,res) = List.fold_left f base args in res in
//│ │ ^
//│ ▼
//│ ◉ (_ -> ?a -> _) comes from
//│ ◉ (_ -> ?c -> _) comes from
//│ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ ^^^^^^^^^^^^^^
//│ ◉ (?a -> _) comes from
//│ ◉ (?c -> _) comes from
//│ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ ^^^^^^^^
//│ ◉ (?a) is assumed for
//│ ◉ (?a -> _) comes from
//│ ◉ (?c) is assumed for
//│ ◉ (?c -> _) comes from
//│ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ ^^^^^^^^
//│ ◉ (_ -> ?a -> _) comes from
//│ ◉ (_ -> ?c -> _) comes from
//│ ▲ - lib. let List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
//│ │ ^^^^^^^^^^^^^^
//│ │ - l.29 let (_,res) = List.fold_left f base args in res in
//│ │ ^
//│ │
//│ ◉ (_ -> ?b -> _) comes from
//│ ◉ (_ -> ?a -> _) comes from
//│ - l.17 let f a x =
//│ ^^^^^
//│ let (carry,currentSum) = a in ...
//│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ◉ (?b -> _) comes from
//│ ◉ (?a -> _) comes from
//│ - l.17 let f a x =
//│ ^^^
//│ let (carry,currentSum) = a in ...
//│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
//│ ◉ (?b) is assumed for
//│ ◉ (?a) is assumed for
//│ │ - l.17 let f a x =
//│ │ ^
//│ │ - l.22 (let (toSum1,toSum2) = x in
Expand All @@ -181,9 +181,9 @@ let bigAdd l1 l2 =
//│ ◉ (_ * _) comes from
//│ - l.22 (let (toSum1,toSum2) = x in
//│ ^^^^^^^^^^^^^^^
//│ U max: 33, total: 532
//│ U max: 33, total: 505
//│ UERR 3 errors
//│ L: 2 [([α127''], [α128''],) ~ list['a141''], [([α127''], [α128''],) - list[([α127''], [α128''],)] ~ list[α144''] - α144'', L: 0 [list[([α127''], [α128''],)] ~ list[α144''], list[([α127''], [α128''],)] <: list[α144'']]], [α144'' - list[α144''] ~ list[α130''] - α130'', L: 0 [list[α144''] ~ list[α130''], list[α144''] <: list[α130'']]], [α130'' - (α130'' -> α129'') ~ (α138'' -> α135'') - α138'', L: 1 [(α130'' -> α129'') ~ (α138'' -> α135''), [(α130'' -> α129'') - (α129'' -> (α130'' -> α129'')) ~ (α131'' -> (α138'' -> α135'')) - (α138'' -> α135''), L: 0 [(α129'' -> (α130'' -> α129'')) ~ (α131'' -> (α138'' -> α135'')), (α129'' -> (α130'' -> α129'')) :> (α131'' -> (α138'' -> α135''))]]]], α138'' <: α142'', α142'' :> list['a141'']]
//│ L: 2 [list['a141''] ~ ([α139''], [α140''],), list['a141''] <: α142'', α142'' :> α138'', [α138'' - (α138'' -> α135'') ~ (α130'' -> α129'') - α130'', L: 1 [(α138'' -> α135'') ~ (α130'' -> α129''), [(α138'' -> α135'') - (α131'' -> (α138'' -> α135'')) ~ (α129'' -> (α130'' -> α129'')) - (α130'' -> α129''), L: 0 [(α131'' -> (α138'' -> α135'')) ~ (α129'' -> (α130'' -> α129'')), (α131'' -> (α138'' -> α135'')) <: (α129'' -> (α130'' -> α129''))]]]], [α130'' - (α130'' -> α129'') ~ (α138'' -> α135'') - α138'', L: 1 [(α130'' -> α129'') ~ (α138'' -> α135''), [(α130'' -> α129'') - (α129'' -> (α130'' -> α129'')) ~ (α131'' -> (α138'' -> α135'')) - (α138'' -> α135''), L: 0 [(α129'' -> (α130'' -> α129'')) ~ (α131'' -> (α138'' -> α135'')), (α129'' -> (α130'' -> α129'')) :> (α131'' -> (α138'' -> α135''))]]]], α138'' <: ([α139''], [α140''],)]
//│ L: 0 [list['a118'''] ~ ([α122'''], [α123'''],), list['a118'''] <: α117''', α117''' :> α113''', α113''' <: ([α122'''], [α123'''],)]
//│ L: 2 [([α121''], [α122''],) ~ list['a134''], [([α121''], [α122''],) - list[([α121''], [α122''],)] ~ list[α137''] - α137'', L: 0 [list[([α121''], [α122''],)] ~ list[α137''], list[([α121''], [α122''],)] <: list[α137'']]], [α137'' - list[α137''] ~ list[α124''] - α124'', L: 0 [list[α137''] ~ list[α124''], list[α137''] <: list[α124'']]], [α124'' - (α124'' -> α123'') ~ (α131'' -> α129'') - α131'', L: 1 [(α124'' -> α123'') ~ (α131'' -> α129''), [(α124'' -> α123'') - (α123'' -> (α124'' -> α123'')) ~ (α125'' -> (α131'' -> α129'')) - (α131'' -> α129''), L: 0 [(α123'' -> (α124'' -> α123'')) ~ (α125'' -> (α131'' -> α129'')), (α123'' -> (α124'' -> α123'')) :> (α125'' -> (α131'' -> α129''))]]]], α131'' <: α135'', α135'' :> list['a134'']]
//│ L: 0 [list['a114'''] ~ ([α117'''], [α118'''],), list['a114'''] <: α113''', α113''' :> α109''', α109''' <: ([α117'''], [α118'''],)]
//│ L: 2 [list['a134''] ~ ([α132''], [α133''],), list['a134''] <: α135'', α135'' :> α131'', [α131'' - (α131'' -> α129'') ~ (α124'' -> α123'') - α124'', L: 1 [(α131'' -> α129'') ~ (α124'' -> α123''), [(α131'' -> α129'') - (α125'' -> (α131'' -> α129'')) ~ (α123'' -> (α124'' -> α123'')) - (α124'' -> α123''), L: 0 [(α125'' -> (α131'' -> α129'')) ~ (α123'' -> (α124'' -> α123'')), (α125'' -> (α131'' -> α129'')) <: (α123'' -> (α124'' -> α123''))]]]], [α124'' - (α124'' -> α123'') ~ (α131'' -> α129'') - α131'', L: 1 [(α124'' -> α123'') ~ (α131'' -> α129''), [(α124'' -> α123'') - (α123'' -> (α124'' -> α123'')) ~ (α125'' -> (α131'' -> α129'')) - (α131'' -> α129''), L: 0 [(α123'' -> (α124'' -> α123'')) ~ (α125'' -> (α131'' -> α129'')), (α123'' -> (α124'' -> α123'')) :> (α125'' -> (α131'' -> α129''))]]]], α131'' <: ([α132''], [α133''],)]

6 changes: 3 additions & 3 deletions shared/src/test/diff/ocaml/SurveyMed2.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ let rec mulByDigit i l =
//│ ◉ (int) comes from
//│ - lib. let ( * ): int -> int -> int
//│ ^^^
//│ U max: 5, total: 58
//│ U max: 5, total: 56
//│ UERR 2 errors
//│ L: 0 [(α62' -> [(list[α63'] -> list[α64'])]) ~ int, (α62' -> [(list[α63'] -> list[α64'])]) <: α59', α59' <: int]
//│ L: 0 [list[[int]] ~ int, list[[int]] <: α60', α60' <: int]
//│ L: 0 [list[[int]] ~ int, list[[int]] <: α58', α58' <: int]
//│ L: 0 [(α60' -> [(list[α61'] -> list[α62'])]) ~ int, (α60' -> [(list[α61'] -> list[α62'])]) <: α57', α57' <: int]

4 changes: 2 additions & 2 deletions shared/src/test/diff/ocaml/SurveyMed3.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,6 @@ let rec additivePersistence n =
//│ ◉ (int) comes from
//│ - l.12 | [] -> 0
//│ ^
//│ U max: 5, total: 115
//│ U max: 5, total: 109
//│ UERR 1 errors
//│ L: 0 [bool ~ int, bool <: α90', α90' <: α80', α80' :> int]
//│ L: 0 [bool ~ int, bool <: α89', α89' <: α80', α80' :> int]

0 comments on commit 7b36b55

Please sign in to comment.