Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005853OCamlOCaml typingpublic2012-12-13 09:402013-04-23 02:43
Reporterelectreg 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
Platformamd64OSLinuxOS Versionubuntu-12.04
Product Version4.00.1 
Target VersionFixed in Version 
Summary0005853: compiler is unable to detect unused cases in pattern matching on GADT
DescriptionSometimes 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 ReproduceCopy-paste code from description and try to run it.
TagsNo tags attached.
Attached Files

- Relationships
related to 0005892resolvedgarrigue GADT exhaustiveness check is broken 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker