Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007863OCamltypingpublic2018-10-16 21:252018-10-17 06:52
Reporterivg 
Assigned Tolpw25 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.05.0 
Target VersionFixed in Version 
Summary0007863: Unexpected interaction with type definitions and GADT refutability checks
DescriptionNote, 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 -> ()
    | _ -> .
```
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019415)
lpw25 (developer)
2018-10-16 21:44

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.
(0019416)
gasche (administrator)
2018-10-16 22:10

module M
: sig
   type t = A
   type u = A
end
= struct
  type t = A
  type u = t = A
end;;
(0019417)
ivg (reporter)
2018-10-16 22:19

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]
```
(0019418)
garrigue (manager)
2018-10-17 04:26

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?
(0019419)
gasche (administrator)
2018-10-17 06:52

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

- Issue History
Date Modified Username Field Change
2018-10-16 21:25 ivg New Issue
2018-10-16 21:44 lpw25 Note Added: 0019415
2018-10-16 21:45 lpw25 Status new => resolved
2018-10-16 21:45 lpw25 Resolution open => no change required
2018-10-16 21:45 lpw25 Assigned To => lpw25
2018-10-16 22:10 gasche Note Added: 0019416
2018-10-16 22:19 ivg Note Added: 0019417
2018-10-17 04:26 garrigue Note Added: 0019418
2018-10-17 06:52 gasche Note Added: 0019419


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker