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

Wish: implicit identity coercion in pattern-matching #7960

Open
vicuna opened this Issue Nov 26, 2002 · 1 comment

Comments

Projects
None yet
1 participant
@vicuna
Copy link
Collaborator

vicuna commented Nov 26, 2002

Original bug ID: 1485
Reporter: administrator
Status: acknowledged
Resolution: open
Priority: normal
Severity: feature
Category: typing

Bug description

Full_Name: Hugo Herbelin
Version: 3.06
OS:
Submission from: herbelin.net1.nerim.net (62.212.105.93)

Bonjour,

I fell on the following curiosity where f : int foo -> bool -> (int * bool)
foo compiles fine but g not.

Regards,

Hugo

type 'a foo = A of 'a | B1 | B2 | B3 | B4 | B5 | B6 | B7 | B8

let f (x:int foo) (y:bool) = match (x,y) with
| A n, b -> A (n,b)
| (B1 | B2 | B3 | B4 | B5 | B6 | B7 | B8 as t), _ -> t

let g (x:int foo) (y:bool) = match (x,y) with
| A n, b -> A (n,b)
| t, _ -> t

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 26, 2002

Comment author: administrator

Full_Name: Hugo Herbelin
Version: 3.06
OS:
Submission from: herbelin.net1.nerim.net (62.212.105.93)

Bonjour,

I fell on the following curiosity where f : int foo -> bool -> (int * bool)
foo compiles fine but g not.

Regards,

Hugo

type 'a foo = A of 'a | B1 | B2 | B3 | B4 | B5 | B6 | B7 | B8

let f (x:int foo) (y:bool) = match (x,y) with
| A n, b -> A (n,b)
| (B1 | B2 | B3 | B4 | B5 | B6 | B7 | B8 as t), _ -> t

let g (x:int foo) (y:bool) = match (x,y) with
| A n, b -> A (n,b)
| t, _ -> t

A story of half-empty or half-full bottle.

Another point of view is that you can be glad that f compiles....

Let us forget about typing constaints first.
More precisely, when you write

| (B1 | B2 | B3 | B4 | B5 | B6 | B7 | B8 as t), _ -> t
^
The type of ``t'' is a type scheme
forall alpha.alpha foo, such a precise type can be built from
the pattern itself.

By contrast, when you write
| t, _ -> t
^
The type of t is some non-generalizable type variable.
Then (well at some point) it unifies both
with the types of ``x'' [int foo] and with the type of A (n,b) [(int

  • bool) foo]. Hence, g fails to typecheck...

Ok you tell me : but I there are type constraints....

My first answer would be : do not use them ! They have no clear
semantics. When some program does not typecheck, you cannot be sure
that adding constraints will make it typecheck.

My second answer would be that some people in the team are working
hard on type constraints
(or at least on solving some typing problem using then). I'll
let them answer more, perhaps there is a solution here.

Merci d'avoir soulevé ce lièvre....

--Luc

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.