Marc Weber wrote:
== main.urs == val main : unit -> transaction page val recIdTopLevel: a ::: Type -> a -> a== main.ur == fun recIdTopLevel [a] b = b fun main () : transaction page = let fun recId [a ::: Type] (b:a) : a = b in return<xml><head></head> <body> {[ (recId 7) ]}<< ok {[ (recIdTopLevel 7) ]}<< fails see below </body> </xml> end ERROR: main.ur|41 col 14| 41:27: Substitution in constructor is blocked by a too-deep unification variable || Replacement:<UNIF:U127::<UNIF:X>> || Body: (<UNIF:P::Type> -> <UNIF:P::Type>) Note: recIdTopLevel and recId should behave the same way. However only recId compiles (?!)
The important difference between the two definitions is that [recId] has explicit type annotations for arguments and return type, while [recIdTopLevel] doesn't. Type inference for Ur is undecidable, so sometimes you need to annotate to satisfy the type checker.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
