Failure to eliminate pattern case when matching by type about idris2

[tauroid]

The error still occurs when I replace (ra,rb) by pair and use fst pair and snd pair in the rhs.

[gallais]

Each clause is checked in isolation: the catchall does not get to know that Pair a b has already
been matched.

The solution is to define a view. There are a number of additional subtleties (such as the fact that
the wrong case tree gets generated if you use a with, or the lack of eta making some definitions
too strict) so you need to define a bunch of auxiliary functions to guide Idris the right way.

This works:

  constructor MkRecord
  someStuff : List String

data View : Type -> Type where
  APair : (a, b : Type) -> View (Pair a b)
  Other : (a : Type) -> View a

view : (a : Type) -> View a
view (Pair a b) = APair a b
view x = Other x

tupleToTupleOfRecordsV : View ty -> ty -> Type
tupleToTupleOfRecords : (t : Type) -> (v : t) -> Type

tupleToTupleOfRecordsV (APair ta tb) v = Pair (Record ta (fst v)) $ tupleToTupleOfRecords tb (snd v)
tupleToTupleOfRecordsV (Other ty) v = Record ty v

tupleToTupleOfRecords t v = tupleToTupleOfRecordsV (view t) v

makeTupleRecord : (t : Type) -> (v : t) -> tupleToTupleOfRecords t v -> Record t v
makeTupleRecord t@_ v rs with (view t)
  _ | APair ta tb = MkRecord (someStuff (fst rs) <+> (makeTupleRecord tb _ (snd rs)).someStuff)
  _ | Other ty = rs

[tauroid]

Thank you! I understand. This must be the first situation I encounter where I match, with a catchall, on a variable which affects the type of the result. I can also see that this isn't special to Type, as I assumed it was; this also gives a similar error:

data X = A | B

t : X -> Type
t A = Int
t B = Bool

f : (x : X) -> t x
f A = 3
f x = True

While processing right hand side of f. Can't solve constraint between: Bool and t x.
     
match.idr:9:7--9:11
   |
 9 | f x = True
   |       ^^^^

Thank you for providing a solution as well! I think the missing piece was that the typechecker needs positive information about how the value was constructed to compute the dependent type, rather than accumulating a negative case list like I thought it might. I guess tupleToTupleOfRecords using view t in its body allows the definite constructor of view t in the case match to carry through into tupleToTupleOfRecordsV? No worries if it's not quite that simple, I know basically nothing about how the unifier works so can pick it up in my own time.