0005927: Type equality broken for conjunctive polymorphic variant tags

(0008878)
lpw25 (developer)
2013-02-19 20:28

I've attached a new fix that is probably more consistent with other behaviour.

(0008880)
garrigue (manager)
2013-02-20 07:40

Actually, the failure in this case is intentional, as this conjunction is clearly impossible.
On the other hand, it could be accepted in a more general way: & t1 is probably equivalent to & t2 for any t1 and t2...
(Oops, there is also the problem of free variables)

(0008882)
lpw25 (developer)
2013-02-20 12:51

Even if the conjunction is impossible, the type itself is valid and should at least be considered equivalent to itself.

Also, the current error is unclear and only occurs during module inclusion checks. For example:

  # module type S = sig type 'a foo constraint 'a = [< `Tag of & int ] end;;
  Error: Module type declarations do not match:
           module type S =
             sig type 'a foo constraint 'a = [< `Tag of & int ] end
         does not match
           module type S =
             sig type 'a foo constraint 'a = [< `Tag of & int ] end
         At position module type S = <here>
         Modules do not match:
           sig type 'a foo constraint 'a = [< `Tag of & int ] end
         is not included in
           sig type 'a foo constraint 'a = [< `Tag of & int ] end
         At position module type S = <here>
         Type declarations do not match:
           type 'a foo constraint 'a = [< `Tag of & int ]
         is not included in
           type 'a foo constraint 'a = [< `Tag of & int ]
         Their constraints differ.

(0017650)
garrigue (manager)
2017-03-14 11:20

Fixed by commit c21ffce, in a slightly more general way.

Issue History
Date Modified	Username	Field	Change
2013-02-19 19:58	lpw25	New Issue
2013-02-19 19:58	lpw25	File Added: fix-amp-equal.diff
2013-02-19 20:27	lpw25	File Added: fix-amp-equal2.diff
2013-02-19 20:28	lpw25	Note Added: 0008878
2013-02-20 07:40	garrigue	Note Added: 0008880
2013-02-20 07:40	garrigue	Assigned To	=> garrigue
2013-02-20 07:40	garrigue	Status	new => acknowledged
2013-02-20 12:51	lpw25	Note Added: 0008882
2013-07-12 09:33	doligez	Target Version	=> 4.02.0+dev
2013-07-12 18:15	doligez	Target Version	4.02.0+dev => 4.01.1+dev
2013-12-16 14:17	doligez	Tag Attached: patch
2014-05-25 20:20	doligez	Target Version	4.01.1+dev => 4.02.0+dev
2014-07-30 20:55	doligez	Target Version	4.02.0+dev => 4.03.0+dev / +beta1
2016-04-18 16:37	doligez	Target Version	4.03.0+dev / +beta1 => 4.03.1+dev
2017-02-16 14:01	doligez	Target Version	4.03.1+dev => undecided
2017-02-23 16:45	doligez	Category	OCaml typing => typing
2017-03-14 11:20	garrigue	Note Added: 0017650
2017-03-14 11:20	garrigue	Status	acknowledged => resolved
2017-03-14 11:20	garrigue	Fixed in Version	=> 4.06.0 +dev/beta1/beta2/rc1
2017-03-14 11:20	garrigue	Resolution	open => fixed

Notes
(0008878) lpw25 (developer) 2013-02-19 20:28	I've attached a new fix that is probably more consistent with other behaviour.

(0008880) garrigue (manager) 2013-02-20 07:40	Actually, the failure in this case is intentional, as this conjunction is clearly impossible. On the other hand, it could be accepted in a more general way: & t1 is probably equivalent to & t2 for any t1 and t2... (Oops, there is also the problem of free variables)

(0008882) lpw25 (developer) 2013-02-20 12:51	Even if the conjunction is impossible, the type itself is valid and should at least be considered equivalent to itself. Also, the current error is unclear and only occurs during module inclusion checks. For example: # module type S = sig type 'a foo constraint 'a = [< `Tag of & int ] end;; Error: Module type declarations do not match: module type S = sig type 'a foo constraint 'a = [< `Tag of & int ] end does not match module type S = sig type 'a foo constraint 'a = [< `Tag of & int ] end At position module type S = <here> Modules do not match: sig type 'a foo constraint 'a = [< `Tag of & int ] end is not included in sig type 'a foo constraint 'a = [< `Tag of & int ] end At position module type S = <here> Type declarations do not match: type 'a foo constraint 'a = [< `Tag of & int ] is not included in type 'a foo constraint 'a = [< `Tag of & int ] Their constraints differ.

(0017650) garrigue (manager) 2017-03-14 11:20	Fixed by commit c21ffce, in a slightly more general way.

Relationships