Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001485OCamlOCaml generalpublic2002-11-26 16:462002-12-01 17:57
Reporteradministrator 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0001485: Wish: implicit identity coercion in pattern-matching
DescriptionFull_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
 



TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000143)
administrator (administrator)
2002-11-26 17:12

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


- Issue History
Date Modified Username Field Change
2005-11-18 10:13 administrator New Issue


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker