Type refinement in dependent pattern matching

Stream: lean4

[David Thrane Christiansen]

Hello! Sorry if I use Zulip wrong, or if this is answered elsewhere - I'm new to both Lean 4 and Zulip.

I am trying to write one of my standard first projects in a dependently typed language, which is a little simply typed lambda calculus. Part of this is the definition of a little universe, with contexts given as lists of codes and environments defined by recursion over contexts. When I try to write a "lookup" function to project a value out of an environment, the equation compiler fails because the type of my index pattern (which ensures that the context is non-empty) doesn't seem to refine the index of the environment type.

Here's the code:

inductive T where
  | nat : T
  | func : T → T → T

inductive Idx : List T → T → Type where
  | here : Idx (τ :: γ) τ
  | there : Idx γ τ → Idx (σ :: γ) τ

def val : T → Type
  | T.nat      => Nat
  | T.func a b => val a → val b

def env : List T → Type
  | []        => Unit
  | (t :: ts) => val t × env ts

def lookup : env γ → Idx γ τ → val τ
  | (v, ρ), here => v
  | (_, ρ), (there i) => lookup ρ i

The error that I get is on the pattern (v, ρ):

type mismatch
  (v, ρ)
has type
  ?m.1145 × ?m.1148 : Type (max ?u.1154 ?u.1153)
but is expected to have type
  env γ : Type

which looks to me like γ isn't being refined by here. Do I need to do anything special to make this work?

Thank you!

[Kyle Miller]

here is being interpreted as a pattern variable; you want Idx.here for the constructor (or use open Idx).

I have an old version of Lean 4, so it could be different now, but I also had to swap the order of the arguments to get it to work:

def lookup : Idx γ τ → env γ → val τ
  | Idx.here, (v, ρ) => v
  | (Idx.there i), (_, ρ) => lookup i ρ

[David Thrane Christiansen]

Thanks for the help! That makes perfect sense. I also have to put the index first to get it to go through.

[Sebastian Ullrich]

Hi David! Note that if you put the index first, Lean even gives you a (subtle) hint: here will be highlighted like other variables, while constants like Idx.here are not highlighted. Unfortunately that doesn't work when putting the index second because it aborts before even elaborating the second pattern, so there is no semantic highlighting. But as you found out, that order doesn't quite work anyway.