New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type inference leaves unsolved uvars and crashes #1443

Closed
nikswamy opened this Issue Apr 30, 2018 · 6 comments

Comments

Projects
None yet
5 participants
@nikswamy
Contributor

nikswamy commented Apr 30, 2018

module Test
let rec test ps = match ps with
  | [] -> 0
  | a::q ->
    let rec blah i = match i with
      | [] -> 0
      | b::r -> blah r
    in
    if a = 0 then 0
    else test q

Failure("(Test.fst(6,16-6,17)) CheckNoUvars: Unexpected unification variable remains: (?u1736) _")

Thanks to @R1kM

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido May 9, 2018

Contributor

Still present, here's a minimization:

let test =
   let rec blah i = () in ()

The uvar seems to stem from the type of i, annotating it makes it work. If blah is not rec, we just get:

A.fst(4,17-4,18): (Error 66) Failed to resolve implicit argument ?1593 of type Type introduced for user-provided implicit term

as expected.

Contributor

mtzguido commented May 9, 2018

Still present, here's a minimization:

let test =
   let rec blah i = () in ()

The uvar seems to stem from the type of i, annotating it makes it work. If blah is not rec, we just get:

A.fst(4,17-4,18): (Error 66) Failed to resolve implicit argument ?1593 of type Type introduced for user-provided implicit term

as expected.

@aseemr

This comment has been minimized.

Show comment
Hide comment
@aseemr

aseemr May 10, 2018

Contributor

Isn't it expected given that inner lets are not generalized and here the type of i can't be inferred?

Contributor

aseemr commented May 10, 2018

Isn't it expected given that inner lets are not generalized and here the type of i can't be inferred?

@theolaurent

This comment has been minimized.

Show comment
Hide comment
@theolaurent

theolaurent Jun 5, 2018

An different (?) repro

val foo : unit -> unit
let foo t =
  let rec bar env t = ()
  in bar [] t

It doesn't fail without the first argument:

val foo : unit -> unit
let foo t =
  let rec bar t = ()
  in bar t

But still fails when the let rec is not nested:

let rec bar env t = ()

val foo : unit -> unit
let foo t = bar [] t

(don't know if it is related, but I got the same error a few weeks ago #1423)

theolaurent commented Jun 5, 2018

An different (?) repro

val foo : unit -> unit
let foo t =
  let rec bar env t = ()
  in bar [] t

It doesn't fail without the first argument:

val foo : unit -> unit
let foo t =
  let rec bar t = ()
  in bar t

But still fails when the let rec is not nested:

let rec bar env t = ()

val foo : unit -> unit
let foo t = bar [] t

(don't know if it is related, but I got the same error a few weeks ago #1423)

@lastland

This comment has been minimized.

Show comment
Hide comment
@lastland

lastland Jun 19, 2018

Another example:

noeq type ins 'ins_typ = {
  eval_ins : 'ins_typ -> unit;
  ins_to_string : 'int_typ -> string
}

noeq type add64 't1 't2 = {
  dst: 't1;
  src: 't2
}

assume val eval_add64 : add64 't1 't2 ->  unit

assume val add64_to_string : add64 't1 't2 -> string

let add64_ins (#t1:Type)(#t2:Type) : ins (add64 t1 t2) = {
  eval_ins = eval_add64;
  ins_to_string = add64_to_string
}

Replacing the last definition with the following code would work:

let add64_ins (#t1:Type)(#t2:Type) : ins (add64 t1 t2) = {
  eval_ins = eval_add64;
  ins_to_string = add64_to_string #t1 #t2
}

lastland commented Jun 19, 2018

Another example:

noeq type ins 'ins_typ = {
  eval_ins : 'ins_typ -> unit;
  ins_to_string : 'int_typ -> string
}

noeq type add64 't1 't2 = {
  dst: 't1;
  src: 't2
}

assume val eval_add64 : add64 't1 't2 ->  unit

assume val add64_to_string : add64 't1 't2 -> string

let add64_ins (#t1:Type)(#t2:Type) : ins (add64 t1 t2) = {
  eval_ins = eval_add64;
  ins_to_string = add64_to_string
}

Replacing the last definition with the following code would work:

let add64_ins (#t1:Type)(#t2:Type) : ins (add64 t1 t2) = {
  eval_ins = eval_add64;
  ins_to_string = add64_to_string #t1 #t2
}
@theolaurent

This comment has been minimized.

Show comment
Hide comment
@theolaurent

theolaurent Jul 5, 2018

Yet at different one:

type test (a : unit) =
  | Test : test a

val f : #x:unit -> test x
let f #x = (Test #x)

let g () : unit = match f with
  | Test -> ()

theolaurent commented Jul 5, 2018

Yet at different one:

type test (a : unit) =
  | Test : test a

val f : #x:unit -> test x
let f #x = (Test #x)

let g () : unit = match f with
  | Test -> ()

mtzguido added a commit that referenced this issue Oct 8, 2018

@mtzguido mtzguido self-assigned this Oct 8, 2018

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 8, 2018

Contributor

I'm on this

Contributor

mtzguido commented Oct 8, 2018

I'm on this

mtzguido added a commit that referenced this issue Oct 8, 2018

tc: term: track some implicit in annotations being lost
We were checking the types for each let rec, but not tracking the
implicits that they might have. This is needed, as the many repros in
 #1443 show.

mtzguido added a commit that referenced this issue Oct 8, 2018

tc: rel: tracking implicits that were being lost
Calling solve_t might return new implicits, which we must again keep
track of. To make sure we don't duplicate the implicits we're tracking,
we do the call with an empty list of implicits, and then we append the
result to the implicits we were already carrying.

c.f. #1443 and #1523

mtzguido added a commit that referenced this issue Oct 9, 2018

tc: term: track some implicit in annotations being lost
We were checking the types for each let rec, but not tracking the
implicits that they might have. This is needed, as the many repros in
 #1443 show.

mtzguido added a commit that referenced this issue Oct 9, 2018

tc: rel: tracking implicits that were being lost
Calling solve_t might return new implicits, which we must again keep
track of. To make sure we don't duplicate the implicits we're tracking,
we do the call with an empty list of implicits, and then we append the
result to the implicits we were already carrying.

c.f. #1443 and #1523
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment