Anonymous | Login | Signup for a new account | 2019-02-20 03:09 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | |||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | |||||||
0007617 | OCaml | typing | public | 2017-09-01 18:57 | 2017-09-13 01:34 | |||||||
Reporter | trefis | |||||||||||
Assigned To | garrigue | |||||||||||
Priority | normal | Severity | minor | Reproducibility | always | |||||||
Status | resolved | Resolution | fixed | |||||||||
Platform | OS | OS Version | ||||||||||
Product Version | ||||||||||||
Target Version | Fixed in Version | 4.06.0 +dev/beta1/beta2/rc1 | ||||||||||
Summary | 0007617: Ambiguous type escaping the scope of its equation | |||||||||||
Description | The following example typechecks properly: # type ('a, 'b) eq = Refl : ('a, 'a) eq;; type ('a, 'b) eq = Refl : ('a, 'a) eq # let ok (type a b) (x : (a, b) eq) = match x, [] with | Refl, [(_ : a) | (_ : b)] -> [] ;; val ok : ('a, 'b) eq -> 'c list But I claim it shouldn't as the typechecker will have chosen an arbitrary rigid type for the ambivalent pattern [(_ : a) | (_ : b)]. This is made more apparent with the following examples: # let oks (type a b) (x : (a, b) eq) = match x, [] with | Refl, [(_ : a) | (_ : b)] -> [] | Refl, [(_ : a) | (_ : b)] -> [] ;; val oks : ('a, 'b) eq -> 'c list # let fails (type a b) (x : (a, b) eq) = match x, [] with | Refl, [(_ : a) | (_ : b)] -> [] | Refl, [(_ : b) | (_ : a)] -> [] ;; Error: This pattern matches values of type (a, b) eq * b list but a pattern was expected which matches values of type (a, b) eq * a list Type b is not compatible with type a N.B. this happens both with and without -principal. | |||||||||||
Tags | No tags attached. | |||||||||||
Attached Files | ||||||||||||
![]() |
|
(0018224) garrigue (manager) 2017-09-05 16:24 |
Actually, the first example is fine: since [] has type forall 'a. 'a list, the type is not escaping. But the fails example should not fail. We should use a different instance of the scrutinee for each case. |
(0018229) garrigue (manager) 2017-09-06 09:34 |
Cf. https://github.com/ocaml/ocaml/pull/1318 [^] |
(0018241) garrigue (manager) 2017-09-13 01:34 |
Fixed in trunk by commits 19b37dc5 and 5c174df4. Do not lower the level when unifying branches of pattern-matching together, and use local environment for unification. |
![]() |
|||
Date Modified | Username | Field | Change |
2017-09-01 18:57 | trefis | New Issue | |
2017-09-05 16:24 | garrigue | Note Added: 0018224 | |
2017-09-05 16:24 | garrigue | Assigned To | => garrigue |
2017-09-05 16:24 | garrigue | Status | new => confirmed |
2017-09-05 16:27 | garrigue | Relationship added | parent of 0007618 |
2017-09-06 09:34 | garrigue | Note Added: 0018229 | |
2017-09-13 01:34 | garrigue | Note Added: 0018241 | |
2017-09-13 01:34 | garrigue | Status | confirmed => resolved |
2017-09-13 01:34 | garrigue | Fixed in Version | => 4.06.0 +dev/beta1/beta2/rc1 |
2017-09-13 01:34 | garrigue | Resolution | open => fixed |
Copyright © 2000 - 2011 MantisBT Group |