Skip to content
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

Unable to add multiple constraints/equations to a type #7544

Open
vicuna opened this issue May 30, 2017 · 6 comments
Open

Unable to add multiple constraints/equations to a type #7544

vicuna opened this issue May 30, 2017 · 6 comments

Comments

@vicuna
Copy link

vicuna commented May 30, 2017

Original bug ID: 7544
Reporter: roshanjames
Status: acknowledged (set by @mshinwell on 2017-06-02T14:42:49Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Monitored by: @lpw25

Bug description

In the code below, f does not compile and produces

Error: This expression has type [< `A | `B ] M.t
       but an expression was expected of type [ `A ] M.t
       The second variant type does not allow tag(s) `B

because OCaml is unable to constrain the type of [m] from
[[< `A | `B] M.t] to [[`A] M.t] or [[`B] M.t] in each branch of the
match.

type 'k kind =
  | A : [ `A ] kind
  | B : [ `B ] kind
  | C : [ `C ] kind

module M = struct
  type 'k t = { kind : 'k kind }
end

module P = struct
  type t = T : [< `A | `B ] M.t -> t

  let pack_exn (type k) (m : k M.t) =
    match m.kind with
    | A -> T m
    | B -> T m
    | C -> failwith ""
end

let g (m : [ `A ] M.t) = ()

let f (type k) (m : k M.t) =
  let P.T m = P.pack_exn m in
  match m.kind with
  | A -> g m
  | B -> ()

Here is one more program that fails for the same reason, which wasn't
as obvious to me initially (I got this one from Leo White):

type 'k kind =
    | A : [< `A ] kind
    | A_and_B    : [< `A | `B ] kind

let foo (x : [< `A ]) = ()

let bar1 (type k) (x : k kind) (y : k kind) (z : k) =
  match x, y with
  | A, A_and_B -> foo z
  | _ -> ()

let bar2 (type k) (x : k kind) (y : k kind) (z : k) =
  match x, y with
  | A_and_B, A -> foo z
  | _ -> ()

Here bar1 compiles, but bar2 does not:

Error: This expression has type k but an expression was expected of type
         [< `A ]
       The second variant type does not allow tag(s) `B
@github-actions
Copy link

github-actions bot commented May 8, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 8, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 8, 2020

@garrigue Is this in the class of things that can't really be fixed with the current implementation? I suspect that it might be, but I'd appreciate you confirming that before I close the issue.

@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

Not really. I long thought that it would require changing the behaviour of the expansion of type abbreviations in a row variable position, but actually the more reasonable approach is to have the expansion of this abbreviation replace the whole variant type (which is what is already done in includecore), since we want it to control the presence flag of all fields too. However, this means checking for possible replacement of the whole row in lots of places, possibly all occurrences of row_repr.
Have to sit down and think about it.

@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

This said, I'm not too much excited by all the chances of bugs it will introduce.

@github-actions github-actions bot removed the Stale label Jun 10, 2020
@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label Oct 11, 2021
@garrigue garrigue removed the Stale label Oct 14, 2021
@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label Oct 21, 2022
@garrigue garrigue removed the Stale label Nov 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants