Incorrect elaboration of lambda-case within a parameters block

[ohad]

Steps to Reproduce

-- Works
Fine : Unit -> Nat
Fine = \case
  () => 0

data Good : Type where
  AGood : Good

Works : Good -> Nat
Works = \case
  AGood => 0

parameters (n : Nat)
  FineToo : Unit -> Nat
  FineToo = \case
    () => 0

  data Bad : Type where
    ABad : Bad

  failing
    Fails : Bad -> Nat
    Fails = \case
      ABad => 0

Expected Behavior

Everything should work.

Observed Behavior

Uncommenting the failing block fails. Moreover, the error we report is about the Bad data declaration:

   While processing right hand side of Fails. When unifying:
         Type
     and:
         ?argTy -> Type
     Mismatch between: Type and ?argTy -> Type.
     
     MoreParam:18:3--19:15
      18 |   data Bad : Type where
      19 |     ABad : Bad

[dunhamsteve]

Given:

parameters (n : Nat)
  data Bad : Type where
    ABad : Bad

I get:

:t ABad
Main.ABad : (n : Nat) -> Bad n

Is this how parameter blocks are supposed to work or is it being too aggressive?

[ohad]

@dunhamsteve I think this is how they're meant to work. What would be an alternative?

Making n implicit in ABad seems like guesswork, in the sense that we'll always have cases where we'll want it to be explicit.

[ohad]

pour @edwinb

import Data.Vect

foo : (n : Nat) -> Bool
foo n = ?h1
  where
    data Bad : Type where
      ABad : Vect n a -> Bad

    Fails : Bad -> Nat
    Fails = \case
      ABad xs => 0

failing "Mismatch between: Type and ?argTy -> Type."
  parameters (n : Nat)
    data Bad' : Type where
      ABad' : Vect n a -> Bad'

    Fails : Bad' -> Nat
    Fails = \case
      ABad' xs => 0

[dunhamsteve]

Yeah, I just wasn't sure if parameters were supposed to apply to constructors. I think I've got a good mental model now. They're added to constructors and functions and are automatically filled in for applications using the same NestedNames mechanism that is used for lifting local definitions.

Your test case also fails with a normal (non-lambda) case statement, but works for top level function definitions.

I've been looking into this a little in my off hours to learn how Idris2 works, but I keep deferring adding a comment because there is always one more thing I want to look at. It case it helps, this is what I've seen so far:

Case.idr never makes it to the "Expected scrutinee type" message. It's failing here: https://github.com/idris-lang/Idris2/blob/30866fa89297ebf1d991d75b34e4cf2e7b12733c/src/TTImp/Elab/Case.idr#L396-L397

scrty_exp is ($resolved2556 ?). And $resolved2556 is Bad and is in nest. The ? is added here:

https://github.com/idris-lang/Idris2/blob/30866fa89297ebf1d991d75b34e4cf2e7b12733c/src/TTImp/Elab/Case.idr#L463

I think some code (check) is treating the $resolved2556 as if it had the n tacked on, and other code (guessScrType) is not. So guessScrType thinks it needs an arg, but check does not (or rather adds the n to the expression during checking). I'm not sure if we're supposed to expect check to sort that out or to get guessScrType to return a $resolved2556.

In the latter case, I've tweaked getRetTy locally to look into nest and use tmf EmptyFC Func (cribbed from envHints in Check.idr). I had to believe_me some vars away, so it was just to see what happens before trying to sort that out. This change gets the $resolved2556 returned and gets through that check in both of your cases, but I have a subsequent failure on the LHS of the case alts. I suspect a similar issue there, but had to go to bed (and now its time for work).

Maybe this info will help somebody who knows more than me, but I'll poke at it a bit more later. This problem may go away or change shape with new core, so this all could be an academic exercise.