French quotes can lead to unexpected evaluation.

[ratmice]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This is perhaps not a bug, but underhanded usage of french quotes can lead to results contrary to what one might expect from a naive reading of the sources,

for an example, the following sources the last line evaluates to "foo" -- which is understandable since constT A C and constT A B both elaborate to A.

Steps to Reproduce

variables {A B C: Type} def pick_one: A → A → A := λ _ _, ‹A›. def constT: Type -> Type -> Type := λ t1, λ t2, t1. def mkConstT: A -> B -> constT A B := λ _ _, ‹A›. def underhanded: constT A B -> constT A C -> A := λ _ _, ‹constT A C›. #eval (pick_one "foo" "bar") #eval (underhanded (mkConstT "foo" ()) (mkConstT "bar" true))

Expected behavior: I would probably expect it to evaluate the last line to "bar"

Actual behavior: evaluates the last line to "foo"

Reproduces how often: always

Versions

Tested on the web version.