Stream: Coq users

Topic: Need eq to unfold?

Shea Levy (Oct 15 2020 at 20:41):

I have a use case where I need to do something like

match (eq_refl : foo = bar) in _ = bar return bar with
| eq_refl => my_foo
end

to get a term to typecheck (my_foo alone fails). Is this a bug? I can try to make a minimal example but this seems really odd that eq_refl is typechecking but I can't just use the term directly.

Gaëtan Gilbert (Oct 15 2020 at 20:49):

weird
what about (my_foo : foo) : bar and my_foo : bar?

Shea Levy (Oct 15 2020 at 21:14):

First one works!

Shea Levy (Oct 15 2020 at 21:14):

Oh so does second one, I thought I'd tried that...

Shea Levy (Oct 15 2020 at 21:15):

But without the cast it fails

Gaëtan Gilbert (Oct 15 2020 at 21:18):

what failure?
are you just doing Check my_foo or something more complicated?

Shea Levy (Oct 15 2020 at 21:21):

Require Import Unicode.Utf8.

Inductive composition_endpoints : nat → Type :=
| both_endpoints_same : Type → composition_endpoints 0
| endpoints_are : ∀ {n}, Type → Type → composition_endpoints (S n).

Definition compose_type n (ce : composition_endpoints n) :=
  let
    (dom, cod) := match ce with
                  | both_endpoints_same A => (A, A)
                  | endpoints_are A B => (A, B)
                  end
  in (fix compose_type' n dom' :=
        match n with
        | 0 => dom → dom'
        | S n' =>
          let
            go cod := (dom' → cod) → compose_type' n' cod
          in match n' with
             | 0 => go cod
             | _ => ∀ cod, go cod
             end
        end
     ) n dom.

Fixpoint compose n : ∀ ce, compose_type n ce :=
  match n with
  | 0 =>
    λ ce,
    match ce with
    | both_endpoints_same T =>
      ((λ (x : T), x) : compose_type 0 (both_endpoints_same T))
    end
  | S n' => _
  end.

If I remove the cast near the bottom (but keep the fully typed binding on the lambda) I get:

Error: The type of this term is a product while it is expected to be
(compose_type ?n0@{y0:=0} ?c@{y0:=0; c0:=both_endpoints_same T}).

Paolo Giarrusso (Oct 15 2020 at 22:03):

The errore seems accurate? compose_type n isn't definitionally a product type.

Paolo Giarrusso (Oct 15 2020 at 22:04):

That is, if n is a Coq variable.

Paolo Giarrusso (Oct 15 2020 at 22:05):

If you apply to a number starting with a constructor, then it's probably a product again (and clearly so for 0)

Shea Levy (Oct 15 2020 at 22:24):

But in context I know n is 0, it's instantiated as such.

Jasper Hugunin (Oct 15 2020 at 22:28):

If you annotate match n with as match n return forall ce, compose_type n ce with, does it go through? Or do you need to also add match ce return compose_type 0 ce with?

Paolo Giarrusso (Oct 15 2020 at 22:43):

@Shea Levy not necessarily, without full GADT semantics or the appropriate return type annotation for match: match n as n0 return ... compose_type n0 ...

Paolo Giarrusso (Oct 15 2020 at 22:46):

Stronger inference algorithms exist, including in Equations, but it's not unusual to need annotations in such cases (even simpler ones)

Paolo Giarrusso (Oct 15 2020 at 22:48):

In your case, Coq knows that it must substitute 0 for y0 in ?n0, but it hasn't yet decided what to unify n0 with.

Shea Levy (Oct 15 2020 at 23:17):

Hmm this worked (with the explicit idProp line for the other ctor):

    match ce as ce' in composition_endpoints n' return match n' with
                                                       | 0 => compose_type 0
                                                       | S _ => λ ce, IDProp
                                                       end ce' with

Last updated: Sep 30 2023 at 06:01 UTC