Add another test that exhibits a similar problem.

This commit is contained in:
François Pottier 2022-04-06 22:22:48 +02:00
parent df673337a8
commit 3ec62a9c73
2 changed files with 23 additions and 0 deletions

View File

@ -0,0 +1,4 @@
(* We have unreachable generalizable variables inside the left-hand
side of a [letr] combinator. *)
let _ =
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()

View File

@ -315,6 +315,25 @@ It involves a useless universal quantifier.
Converting the System F term to de Bruijn style...
Type-checking the System F term...
This example is also correct.
It involves unreachable generalizable type variables,
that is, type variables that are both unconstrained
and unreachable from the entry point of a type scheme.
$ cat rigid-unreachable.midml
(* We have unreachable generalizable variables inside the left-hand
side of a [letr] combinator. *)
let _ =
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()
$ midml rigid-unreachable.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN b -> (FUN a0 -> (FUN a1 -> (fun (x : a1) -> x : a1 -> a1))) [{}] [b] ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
The example below is incorrect, it tries to unify two distinct rigid
variables.