0001485: Wish: implicit identity coercion in pattern-matching

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

Relationships