[Ur] Pattern Matching

[Adam Chlipala]

Ur type inference is defined never to deduce the presence of 
polymorphism.  Rather, polymorphism is always declared explicitly.

In contrast to, say, ML, type inference in Ur is undecidable, hence the 
requirement that the program give more annotations.

On 05/29/2013 09:57 AM, David Snider wrote:
> Let's say I rewrite that as:
>
> fun zip a b =
>   case (a, b) of
>       (a :: as, b :: bs) => (a, b) :: zip as bs
>     | _ => []
>
> This throws a unification failure until I write:
>
> fun blah () = (zip (1::[]) (2::[]))
>
> At which point the compiler is able to infer the types and all 
> compiles correctly
>
> Is there some reason that the compiler can't/shouldn't default to:
>
> fun zip [t] [t2] (a : list t) (b : list t2) : list (t * t2) =
>   case (a, b) of
>       (a :: as, b :: bs) => (a, b) :: zip as bs
>     | _ => []
>
> when unification isn't possible?