Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007618OCamltypingpublic2017-09-01 18:592017-09-13 01:34
Reportertrefis 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.06.0 +dev/beta1/beta2/rc1 
Summary0007618: Unexpected GADT error
DescriptionCurrently the following code is rejected by the typechecker:

    # type _ t = I : int t
    type _ t = I : int t
    # let f (type a) (x : a t) (y : int) =
        match x, y with
        | I, (_:a) -> ()
      ;;
    Error: This pattern matches values of type a t * a
           but a pattern was expected which matches values of type a t * int
           Type a is not compatible with type int

While this one is accepted:

    # let g (type a) (x : a t) (y : a) =
        match x, y with
        | I, (0:int) -> ()
      ;;
    val g : 'a t -> 'a -> unit

I believe that both of these function suffer from the issue raised in 0007617,
i.e. the typechecker allows ambiguous types to escape, arbitrarily choosing one
of the instances as the type of the pattern (or rather, always choosing the
locally abstract type).

[f] later fails to typecheck because we try to unify the type of the pattern
with the type of the argument outside the scope of the equation introduced by
[I].
This happens on line 3887 of typecore.ml, with the call to
[unify_pats (instance env ty_arg)].

Once 0007617 is fixed, everything else being unchanged, these functions should
both be rejected.
However Leo suggests they could be accepted that the typechecker if we decreased
the sharing between the type of the scrutiny and the expected type of each
pattern (eg. by using generalize_structure).
TagsNo tags attached.
Attached Files

- Relationships
child of 0007617resolvedgarrigue Ambiguous type escaping the scope of its equation 

-  Notes
(0018225)
garrigue (manager)
2017-09-05 16:27

Leo is right. The fix should be the same as 7617.
(0018240)
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.

- Issue History
Date Modified Username Field Change
2017-09-01 18:59 trefis New Issue
2017-09-05 16:26 garrigue Relationship added related to 0001617
2017-09-05 16:27 garrigue Note Added: 0018225
2017-09-05 16:27 garrigue Assigned To => garrigue
2017-09-05 16:27 garrigue Status new => confirmed
2017-09-05 16:27 garrigue Relationship deleted related to 0001617
2017-09-05 16:27 garrigue Relationship added child of 0007617
2017-09-13 01:34 garrigue Note Added: 0018240
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
Powered by Mantis Bugtracker