Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Unexpected interaction with type definitions and GADT refutability checks #7863
Original bug ID: 7863
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:
Doesn't type check with an error:
Even if we will put
However, if we will give different names to their corresponding data constructors, e.g.,
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.,
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.
Comment author: @ivg
Yep, this example I was considering, as well as
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.,
Comment author: @garrigue
I've been thinking of removing the exception for abstract types defined in the current module for a long time.