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
compiler is unable to detect unused cases in pattern matching on GADT #5853
Comments
Comment author: @gasche module Nat = struct type z type 'a s end;;include Nat;;type z = Nat.z type ('a, _) iList =
| ICons : 'a * ('a, 'n) iList -> ('a, 'n s) iList;; let hd : type n . ('a, n s) iList -> 'a = function (ICons(x, _)) -> x;;Warning 8: this pattern-matching is not exhaustive. module Nat = struct type z type 'a s end;;include (Nat : module type of Nat);;type z type ('a, _) iList =
| ICons : 'a * ('a, 'n) iList -> ('a, 'n s) iList;; let hd : type n . ('a, n s) iList -> 'a = function (ICons(x, _)) -> x;;val hd : ('a, 'n s) iList -> 'a = |
Comment author: @lpw25 This isn't really a bug, the problem is that your module does not expose the fact that z and s are definitely different types. I think the simplest solution is to change your module to something like: module Nat = struct or if you prefer: module Nat = struct |
Comment author: @gasche Strange, I always assumed that abstract types in signatures and types-without-equations in structures had exactly the same semantics. I find it surprising that the type system has a stronger equational theory in the latter case. |
Comment author: @garrigue Leo described the situation correctly. Just for fun, here is a counter-example showing that your function could be non-exhaustive, assuming the same type for Nat. type (,) eq = Eq : ('a,'a) eq module Nat : sig type (, 'l) iList = let cast_iList : type a b. (a,b) eq -> ('c,a) iList -> ('c,b) iList = let nil : (_, Nat.z Nat.s) iList = cast_iList Nat.eq INil |
Comment author: @gasche (I'm answering here rather than in 5343 to avoid shuffling the bugtracker frontpage too much) Thanks for the answer and interesting reference, But why are module-local abstract types assumed to be contractive? It seems indeed safe to assume that undefined types in structures are contractive, but it would still be simpler and more regular to have them behave just like external abstract types. My guess would be that undefined types in structures are used to introduce primitive types handled by the compiler but defined in libraries rather than in the initial environment, and therefore they need a specific semantic to hide the fact that we don't have the signature language to express contractibility (or, in the present case or in #5361, explicit guarantees of type inequalities). |
Comment author: @garrigue
Concerning contractiveness, actually this is no longer the case. For type equality, the answer is just: because we can. |
Original bug ID: 5853
Reporter: electreg
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:43Z)
Resolution: not a bug
Priority: normal
Severity: minor
Platform: amd64
OS: Linux
OS Version: ubuntu-12.04
Version: 4.00.1
Category: typing
Related to: #5892
Child of: #5998
Bug description
Sometimes compiler gives "Warning 8: this pattern-matching is not exhaustive." when it is not true.
I tried to make Nat-indexed list:
module Nat = struct
type z
type 'a s
end
type (, 'l) iList =
| INil : (, Nat.z) iList
| ICons : 'a * ('a, 'n) iList -> ('a, 'n Nat.s) iList
and then write "safe head" function:
let hd : ('a, 'n Nat.s) iList -> 'a = fun (ICons(x, _)) -> x
So expression
hd INil
is ill-typed; however, compiler gives me "pattern-matching is not exhaustive" warning.Steps to reproduce
Copy-paste code from description and try to run it.
The text was updated successfully, but these errors were encountered: