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

Interaction between GADTs and polymorphic variants #5724

Closed
vicuna opened this issue Aug 14, 2012 · 4 comments
Closed

Interaction between GADTs and polymorphic variants #5724

vicuna opened this issue Aug 14, 2012 · 4 comments
Assignees
Labels
bug typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Aug 14, 2012

Original bug ID: 5724
Reporter: @yallop
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:42Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.00.0
Fixed in version: 4.01.0+dev
Category: ~DO NOT USE (was: OCaml general)
Child of: #5998

Bug description

OCaml reports an error for the last line of the following program:

type _ t =
| A : int t
| B : [`C] -> bool t

let isA (type a) (r : a t) = match r with
| A -> true
| B `C -> false
^^^^
Error: This pattern matches values of type bool t
but a pattern was expected which matches values of type int t

If the `C in the pattern is replaced with an underscore, the program is accepted.

@vicuna
Copy link
Author

vicuna commented Aug 14, 2012

Comment author: @garrigue

This is a documented limitation of GADTs: types cannot be refined if a pattern-matching contains polymorphic variant.
This comes from the fact polymorphic variant pattern-matching typing is specified in the absence of type propagation and GADT type refinement requires type propagation.
This might be improved in the future, but there is no complete solution.

@vicuna
Copy link
Author

vicuna commented Jan 28, 2013

Comment author: @yallop

It's good to see that the trunk typechecker now accepts the example.

@vicuna
Copy link
Author

vicuna commented Jan 29, 2013

Comment author: @garrigue

Re-open before changing resolution.

@vicuna
Copy link
Author

vicuna commented Jan 29, 2013

Comment author: @garrigue

This is now fixed in trunk, since revision 13221.

Here is the corresponding message sent to the caml-list:

As you may be aware from past threads, since the introduction of GADTs
in 4.00, some type information is propagated to pattern-matching, to allow
it to refine types.
More recently, types have started being used to disambiguate constructors
and record fields, which means some more dependency on type information
in pattern-matching.

However, a weakness of this approach was that propagation was disabled
as soon as a pattern contained polymorphic variants. The reason is that
typing rules for polymorphic variants in patterns and expression are subtly
different, and mixing information without care would lose principality.

At long last I have removed this restriction on the presence of polymorphic
variants, but this has some consequences on typing:

  • while type information is now propagated, information about possibly
    present constructors still has to be discarded. For instance this means that
    the following code will not be typed as you could expect:

    let f (x : [< A | B]) = match x with A -> 1 | _ -> 2;; val f : [< A | B > A ] -> int

What happens is that inside pattern-matching, only required constructors
are propagated, which reduces the type of x to [> ] (a polymorphic variant
type with any constructor…)
As before, to give an upper bound to the matched type, the type annotation
must be inside a pattern:

let f = function (`A : [< `A | `B]) -> 1 | _ -> 2;;
val f : [< `A | `B ] -> int = <fun>
  • the propagation of type information may lead to failure in some cases that
    where typable before:

    type ab = [ A | B ];;
    let f (x : [A]) = match x with #ab -> 1;; Error: This pattern matches values of type [? A | B ] but a pattern was expected which matches values of type [ A ]
    The second variant type does not allow tag(s) `B

During pattern-matching it is not allowed to match on absent type constructors,
even though the type of the patterns would eventually be [< A | B], which allows
discarding B. ([? A | `B] denotes a type obeying the rules of pattern-matching)

  • for the sake of coherence, even if a type was not propagated because it
    was not known when typing a pattern-matching, we are still going to fail if a
    matched constructor appears to be absent after typing the whole function.
    (This only applies to propagable types, i.e. polymorphic variant types that
    contain only required constructors)

In particular the last two points are important, because previously such uses
would not have triggered even a warning.

The idea is that allowing propagation of types is more important than
keeping some not really useful corner cases, but if this is of concern
to you, I'm interested in feedback.

@vicuna vicuna closed this as completed Dec 11, 2015
@vicuna vicuna added the bug label Mar 20, 2019
@Octachron Octachron added the typing-GADTS GADT typing and exhaustiveness bugs label May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants