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

Jump to bottom

Unexpected interaction with type definitions and GADT refutability checks #7863

Closed
vicuna opened this issue Oct 16, 2018 · 5 comments
Closed

Unexpected interaction with type definitions and GADT refutability checks #7863

vicuna opened this issue Oct 16, 2018 · 5 comments
Assignees
@lpw25
Labels
bug typing

Comments

@vicuna
Copy link

vicuna commented Oct 16, 2018

Original bug ID: 7863
Reporter: @ivg
Assigned to: @lpw25
Status: resolved (set by @lpw25 on 2018-10-16T19:45:34Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.05.0
Category: typing
Monitored by: @nojb @yallop

Bug description

Note, this issue is reproducible on 4.05 and 4.07 (and probably other versions that I didn't try), but I will showcase using 4.07 since refutation cases provide a nice illustration of the problem.

The unusual thing is that the type checker (or irrefutability checker) depends on the values and the scope of data constructors when it reasons about the possibility of equality of two types. For example, the following code:

module Type = struct
  type 'a value = T1
  type 'a eff = T1
end
open Type


type 'a s = Newtype

type _ term =
  | Val : 'a value s -> 'a value term
  | Eff : 'a eff s  -> 'a eff term

type 'a t = 'a term

let sort : type a. a value t -> unit =
  fun x -> match x with
    | Val x -> ()
    | _ -> .

Doesn't type check with an error:

Error: This match case could not be refuted.
       Here is an example of a value that would reach it: Eff Newtype

Even if we will put 'a value and 'a eff type definitions into different modules, but leave the data constructors names the same, we will still have the same problem.

However, if we will give different names to their corresponding data constructors, e.g.,

module Type = struct
  type 'a value = T1
  type 'a eff = T2
end
open Type


type 'a s = Newtype

type _ term =
  | Val : 'a value s -> 'a value term
  | Eff : 'a eff s  -> 'a eff term

type 'a t = 'a term

let sort : type a. a value t -> unit =
  fun x -> match x with
    | Val x -> ()
    | _ -> .

the refutability check passes.

Another interesting observation is that if we will put the definitions of our phantom types to the toplevel, the refutability check suddenly passes even with equal data constructors, e.g.,

type 'a value = T1
type 'a eff = T1


type 'a s = Newtype

type _ term =
  | Val : 'a value s -> 'a value term
  | Eff : 'a eff s  -> 'a eff term

type 'a t = 'a term

let sort : type a. a value t -> unit =
  fun x -> match x with
    | Val x -> ()
    | _ -> .
@vicuna
Copy link
Author

vicuna commented Oct 16, 2018

Comment author: @lpw25

This is the expected behaviour. Basically, the names of the data constructors is the only way to know for sure that two types aren't equal in any context. The exception is types defined in the current module, where the types can't secretly be equal since we only just defined them.

Personally, I've always disliked the exception for types in the same module as it tends to confuse people. I wouldn't be surprised if it went away some day.

@vicuna vicuna closed this as completed Oct 16, 2018
@vicuna
Copy link
Author

vicuna commented Oct 16, 2018

Comment author: @gasche

module M
: sig
type t = A
type u = A
end
= struct
type t = A
type u = t = A
end;;

@vicuna
Copy link
Author

vicuna commented Oct 16, 2018

Comment author: @ivg

Yep, this example I was considering, as well as type t = | type u = |, no surprises. However, I was expecting that since the module definition is exposed to the type checker it will peek into it. And yes, this same-module heuristic is really confusing, however, I believe that removing it will break so much code, that it is better to deal with it.

Anyway, thanks for the explanation. I wish we had a mechanism in the language for creating unique types that are never equal to each other. So far, the only thing that comes to mind is a ppx_rewriter, that will generate a fresh name, e.g.,

type 'a eff [@@phantom]

@vicuna
Copy link
Author

vicuna commented Oct 17, 2018

Comment author: @garrigue

I've been thinking of removing the exception for abstract types defined in the current module for a long time.
Superficially, it should have very little impact, since this can be only used on small examples.
However, I'm afraid that people still use it to check local properties.
Start by adding a warning?

@vicuna
Copy link
Author

vicuna commented Oct 17, 2018

Comment author: @gasche

I wish we had a mechanism in the language for creating unique types that are never equal to each other.

Yes, we've discussed that several times in the past, a "new" construction that exactly and only does generativity.

@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@lpw25 lpw25

Labels
bug typing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@lpw25 @vicuna