0005853: compiler is unable to detect unused cases in pattern matching on GADT

Notes
(0008599) gasche (developer) 2012-12-13 09:52	# module Nat = struct type z type 'a s end;; # include Nat;; type z = Nat.z type 'a s = 'a Nat.s # type ('a, _) iList = INil : ('b, z) 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. Here is an example of a value that is not matched: INil val hd : ('a, 'n s) iList -> 'a = <fun> # module Nat = struct type z type 'a s end;; # include (Nat : module type of Nat);; type z type 'a s # type ('a, _) iList = INil : ('b, z) 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 = <fun>

(0008600) lpw25 (developer) 2012-12-13 14:26	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 type z = Z type 'a s = S of 'a end or if you prefer: module Nat = struct type z = private Z type 'a s = private S end

(0008602) gasche (developer) 2012-12-13 15:22	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.

(0008606) garrigue (manager) 2012-12-14 03:32	Leo described the situation correctly. Abstract types are only seen as distinct if they are defined in Pervasives or in the local module (i.e. they are guaranteed to have no manifest definition). 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 z type 'a s val eq : (z, 'a s) eq end = struct type z type 'a s = z let eq = Eq end type (_, 'l) iList = \| INil : (_, Nat.z) iList \| ICons : 'a * ('a, 'n) iList -> ('a, 'n Nat.s) iList let cast_iList : type a b. (a,b) eq -> ('c,a) iList -> ('c,b) iList = fun eq l -> let Eq = eq in l let nil : (_, Nat.z Nat.s) iList = cast_iList Nat.eq INil

(0008607) garrigue (manager) 2012-12-14 03:39	By the way, you may also have a look at PR#5343 and its resolution, to see that it is important to distinguish between abstract types in implementations and signatures.

(0008609) gasche (developer) 2012-12-14 11:26	(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 PR#5361, explicit guarantees of type inequalities).

(0008612) garrigue (manager) 2012-12-15 03:33	> 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. Concerning contractiveness, actually this is no longer the case. This would be possible to do that, but we would need to distinguish between types coming from structures and signatures. For type equality, the answer is just: because we can. Initial environment and local modules are the only two cases we can deduce directly from types, without some kind of escape analysis. And having decidable equality for types defined locally is nice for small examples using GADTs. But I agree that it somehow muddles the fact that you need to give a concrete definition for your indices as soon as you use modules.

Issue History
Date Modified	Username	Field	Change
2012-12-13 09:40	electreg	New Issue
2012-12-13 09:52	gasche	Note Added: 0008599
2012-12-13 09:52	gasche	Status	new => acknowledged
2012-12-13 14:26	lpw25	Note Added: 0008600
2012-12-13 15:22	gasche	Note Added: 0008602
2012-12-14 03:32	garrigue	Note Added: 0008606
2012-12-14 03:32	garrigue	Status	acknowledged => resolved
2012-12-14 03:32	garrigue	Resolution	open => no change required
2012-12-14 03:32	garrigue	Assigned To	=> garrigue
2012-12-14 03:39	garrigue	Note Added: 0008607
2012-12-14 11:26	gasche	Note Added: 0008609
2012-12-15 03:33	garrigue	Note Added: 0008612
2013-01-16 15:06	gasche	Relationship added	related to 0005892
2013-04-23 02:43	garrigue	Relationship added	child of 0005998