[Agda] Incompatibilities affecting ``Fresh Look''

[kahl at cas.mcmaster.ca]

On Thu, Dec 16, 2010 at 02:28:06AM +1000, Julian Beaumont wrote:
> 
> Looking at this a little more the following also works:
> 
> just′ : {a : Level} {A : Set a} → A → Maybe A
> just′ x = just x
> 
> drop-just′ : {a : Level} {A : Set a} {x y : A} → just′ x ≡ just′ y → x ≡ y
> drop-just′ refl = refl
> 
> I believe this issue is a result of constructors being overloaded. In
> particular, agda allowing multiple constructors to have the same name

I had not been fully aware of this (I remember reading it, but so far
I have never felt tempted to seriously consider this possibility).
Does anybody have a good use case for that?
(I come from Haskell...)

> and selects the appropriate one for each use site based on the type of
> the result. This prevents agda from deducing the type of "just x"
> since it needs to know [part of] the type of "just x" before it can
> decide which constructor just refers to. Presumably in this case
> there's only one definition of just in scope and so the compiler
> should be able to select it even without knowing the expected type but
> it doesn't appear to do this at the moment.
> 
> In the annotated versions the expected type is known to be "Maybe ?"
> which is enough information for agda to decide which constructor is
> meant by "just x". The version with the just′ function works because
> functions can't be overloaded in the same way constructors can.


Thank you very much for this explanation!


Wolfram