[Agda] Pie in the sky

[Alan Jeffrey]

On 09/24/2010 11:03 AM, Thorsten Altenkirch wrote:
> On 24 Sep 2010, at 15:38, Alan Jeffrey wrote:
>> A simple example of why M shouldn't be typechecked at compile time is a function with type:
>>
>>   f : (x y : T) ->  {x==y ? refl : x == y} ->  U
>
> but we could allow instances of the type for defaults, e.g.
>
> f : (x y : T) ->  {x==y ? refl : x == x} ->  U
>
> which are only used if the application matches the instance.

We might be able to do this example this way, but I suspect in general 
we'd want to show the existence of a unifier which allows the default to 
typecheck.  This sounds pretty hairy to me!

A.