Skip to content
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

Closed
vicuna opened this issue Dec 13, 2012 · 7 comments
Closed

compiler is unable to detect unused cases in pattern matching on GADT #5853

vicuna opened this issue Dec 13, 2012 · 7 comments
Assignees
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Dec 13, 2012

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.

@vicuna
Copy link
Author

vicuna commented Dec 13, 2012

Comment author: @gasche

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 =

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 =

@vicuna
Copy link
Author

vicuna commented Dec 13, 2012

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

@vicuna
Copy link
Author

vicuna commented Dec 13, 2012

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.

@vicuna
Copy link
Author

vicuna commented Dec 14, 2012

Comment author: @garrigue

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

@vicuna
Copy link
Author

vicuna commented Dec 14, 2012

Comment author: @garrigue

By the way, you may also have a look at #5343 and its resolution, to see that it is important to distinguish between abstract types in implementations and signatures.

@vicuna
Copy link
Author

vicuna commented Dec 14, 2012

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

@vicuna
Copy link
Author

vicuna commented Dec 15, 2012

Comment author: @garrigue

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants