Liquidsoap

Type inference doesn't perform enough subtyping

Details

  • Type: Bug Bug
  • Status: Open Open
  • Priority: Major Major
  • Resolution: Unresolved
  • Affects Version/s: 1.0.0-beta3
  • Fix Version/s: None
  • Component/s: Liquidsoap
  • Labels:
    None

Description

The following does not work:
output.dummy(
  fallback([strip_blank(sine()), sine()]),
  fallible=true)
I get:
  this value has type
    source(_)
  but it should be a subtype of (the type of the value at line 1, char 35-42)
    active_source(_)

It is my understanding that there should be no technical reasons to prohibit this and so there must be something to do at the type-checking level..

Edit: The problem is that type inference guesses that this is a list of active_sources, but the second one isn't active; we need a constraint-based type inference algorithm to integrate subtyping in smarter ways, eg. delay the guess until we've seen all elements.

Activity

Ascending order - Click to sort in descending order
Hide
Permalink
Romain Beauxis added a comment -
The issue seems to be around line 532 of lang_values.ml:
  | List l ->
      List.iter (check ~level ~env) l ;
      let pos =
        (* Attach the position of the first item in the list
         * to the type of the list items. It gives more info with type errors
         * when the items in the list are not compatible.
         * WARNING This will become weird with real subtyping in the inference,
         * because the type of elements will only be _a supertype_ of the type
         * of the first item. *)
        match l with e::_ -> e.t.T.pos | [] -> e.t.T.pos
      in
      let v = T.fresh_evar ~level ~pos in
        e.t >: mk (T.List v) ;
        List.iter (fun item -> item.t <: v) l

If I change the previous example to:
output.dummy(
  fallback([fail(), strip_blank(sine()), sine()]),
  fallible=true)

Then it works..
Show
Romain Beauxis added a comment - The issue seems to be around line 532 of lang_values.ml:   | List l ->       List.iter (check ~level ~env) l ;       let pos =         (* Attach the position of the first item in the list          * to the type of the list items. It gives more info with type errors          * when the items in the list are not compatible.          * WARNING This will become weird with real subtyping in the inference,          * because the type of elements will only be _a supertype_ of the type          * of the first item. *)         match l with e::_ -> e.t.T.pos | [] -> e.t.T.pos       in       let v = T.fresh_evar ~level ~pos in         e.t >: mk (T.List v) ;         List.iter (fun item -> item.t <: v) l If I change the previous example to: output.dummy(   fallback([fail(), strip_blank(sine()), sine()]),   fallible=true) Then it works..
Hide
Permalink
David Baelde added a comment -
Yep, I had only seen the problematic example and was about to propose the same workaround. The issue is that our type inference is very shy about subtyping: it sees that strip_blank() produces an active source so it checks that all other sources are active sources. With the first fail(), it gets the type source, and then it is able to see that everything can be seen as a (subtype of) source.

I'm not sure how to fix it quickly, I'm drunk right now ;)
Show
David Baelde added a comment - Yep, I had only seen the problematic example and was about to propose the same workaround. The issue is that our type inference is very shy about subtyping: it sees that strip_blank() produces an active source so it checks that all other sources are active sources. With the first fail(), it gets the type source, and then it is able to see that everything can be seen as a (subtype of) source. I'm not sure how to fix it quickly, I'm drunk right now ;)
David Baelde made changes -
Field Original Value New Value
Assignee David Baelde [ dbaelde ]
David Baelde made changes -
Summary fallback (and possibly other) refuses to start with a mixture of active and regular sources. Type inference doesn't perform enough subtyping
Description The following does not work:
output.dummy(
  fallback([strip_blank(sine()), sine()]),
  fallible=true)
I get:
  this value has type
    source(_)
  but it should be a subtype of (the type of the value at line 1, char 35-42)
    active_source(_)

It is my understanding that there should be no technical reasons to prohibit this and so there must be something to do at the type-checking level..
 The following does not work:
output.dummy(
  fallback([strip_blank(sine()), sine()]),
  fallible=true)
I get:
  this value has type
    source(_)
  but it should be a subtype of (the type of the value at line 1, char 35-42)
    active_source(_)

It is my understanding that there should be no technical reasons to prohibit this and so there must be something to do at the type-checking level..

Edit: The problem is that type inference guesses that this is a list of active_sources, but the second one isn't active; we need a constraint-based type inference algorithm to integrate subtyping in smarter ways, eg. delay the guess until we've seen all elements.
Hide
Permalink
Samuel Mimram added a comment -
Since it seems to hit quite a number of people, couldn't you come up with a quick&dirty patch to handle this case (which really seems the case messing up everybody) and then have a proper fix later?

I don't really like this but I'm afraid that it might take some time to properly fix subtyping...
Show
Samuel Mimram added a comment - Since it seems to hit quite a number of people, couldn't you come up with a quick&dirty patch to handle this case (which really seems the case messing up everybody) and then have a proper fix later? I don't really like this but I'm afraid that it might take some time to properly fix subtyping...
Hide
Permalink
David Baelde added a comment -
Yes, it is possible to not declare strip_blank as active, this will avoid those problems -- not the one that Martin had today, though. I can't think of any major drawback of that solution.

Besides this, I don't see anything convincing. The problem is that our algorithm is local but the problem needs less local insight: when I see an active source, I can't know if it'll need to be subtyped to a normal one. We could use insight from above, eg. say that an active source is always taken as a normal source when inside a list, and this would solve the problem with strip inside fallback, but make it impossible to build lists of active sources, wich may be a problem for some people (Martin, quite likely)...
Show
David Baelde added a comment - Yes, it is possible to not declare strip_blank as active, this will avoid those problems -- not the one that Martin had today, though. I can't think of any major drawback of that solution. Besides this, I don't see anything convincing. The problem is that our algorithm is local but the problem needs less local insight: when I see an active source, I can't know if it'll need to be subtyped to a normal one. We could use insight from above, eg. say that an active source is always taken as a normal source when inside a list, and this would solve the problem with strip inside fallback, but make it impossible to build lists of active sources, wich may be a problem for some people (Martin, quite likely)...
Hide
Permalink
David Baelde added a comment -
I had a little time to kill so I've committed (75110a0ce0e9) the workaround mentioned above: strip_blank now returns a normal source. The problem still holds for examples with lists containing, for example, (active) inputs and normal sources. I'll keep the ticket open until we have a better algorithm.
Show
David Baelde added a comment - I had a little time to kill so I've committed (75110a0ce0e9) the workaround mentioned above: strip_blank now returns a normal source. The problem still holds for examples with lists containing, for example, (active) inputs and normal sources. I'll keep the ticket open until we have a better algorithm.
David Baelde made changes -
Priority Blocker [ 1 ] Major [ 3 ]
Romain Beauxis made changes -
Affects Version/s 1.0.0-beta3 [ 10478 ]
Affects Version/s 1.0 beta [ 10311 ]
Hide
Permalink
Samuel Mimram added a comment -
I just commited a patch in the branch LS-551. It's a hack, but it's simple and correct. What do you think of it?
Show
Samuel Mimram added a comment - I just commited a patch in the branch LS-551 . It's a hack, but it's simple and correct. What do you think of it?

People

  • Assignee:
    David Baelde
    Reporter:
    Romain Beauxis
Vote (0)
Watch (0)

Dates

  • Created:
    Updated: