0007617: Ambiguous type escaping the scope of its equation

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

Relationships

parent of

0007618

resolved

garrigue

Unexpected GADT error

Notes
(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.

Issue History
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