On Sun, Oct 02, 2005 at 10:43:42AM +0200, Jean-Marie Gaillourdet wrote:
> Christian Stork schrieb:
> > Basic Question:  

> >     Why aren't polymorphic variants coerced by default?

> I guess there is some undecidability involved.

My guess too, but I'd like to be sure. ;-)

> > I am automatically generating some code that uses polymorphic variants
> > extensively.  The inferred types are very complicated.  Unfortunatly, at
> > some points in my code coercions are needed for it to compile.  Since I
> > don't have the types available when I generate the code (and I don't
> > think it's possible to refer to inferred types in coercions) I can't
> > coerce explicitly.  I'd like to be able to say something like:

> >     ... f (x: type_of_x :> type_expected_by_f) ...
> Isn't it possible to write something like that:

>  (f: 'a) (x: type_of_x :> 'a)

> I didn't test that trick.

Nice idea.  Let's see:


# type ab  = [ `Apple | `Banana ]
  type abo = [ ab | `Orange]
  let f (x:abo) = match x with #ab -> "ab" | #abo -> "orange"
  let a = (`Apple:ab);;
type ab = [ `Apple | `Banana ]
type abo = [ `Apple | `Banana | `Orange ]
val f : abo -> string = <fun>
val a : ab = `Apple
# f (a:>abo);;
- : string = "ab"
# (f:'a->_) (a:ab:>'a);;
Characters 10-20:
  (f:'a->_) (a:ab:>'a);;
            ^^^^^^^^^^
Type ab = [ `Apple | `Banana ] is not a subtype of type
  abo = [ `Apple | `Banana | `Orange ] 
The first variant type does not allow tag(s) `Orange
# (f:'a->_) (a:>'a);;
Characters 11-12:
  (f:'a->_) (a:>'a);;
             ^
This expression cannot be coerced to type
  abo = [ `Apple | `Banana | `Orange ];
it has type ab but is here used with type abo
The first variant type does not allow tag(s) `Orange


I'm confused about the error message saying that ab is not a subtype of
abo.  I thought it is...

-- 
Chris Stork   <>  Support eff.org!  <>   http://www.ics.uci.edu/~cstork/
OpenPGP fingerprint:  B08B 602C C806 C492 D069  021E 41F3 8C8D 50F9 CA2F