Can't solve constraint between: `[]` and `zipWith _ [] ?_`

[Mr-Andersen]

Steps to Reproduce

git clone https://github.com/Mr-Andersen/hvect1 -b first && cd hvect1 && idris2 --build hvect1.ipkg

Expected Behavior

Builds successfully

Observed Behavior

1/1: Building Main (src/Main.idr)
Error: While processing left hand side of happly. Can't solve constraint
between: [] and zipWith (\a, b => a -> b) [] ?_.

src/Main.idr:13:11--13:13
 09 | happly : {0 k : Nat} -> {0 as, bs : Vect k Type}
 10 |       -> (1 _ : HVect1 as)
 11 |       -> (1 _ : HVect1 (zipWith (\a, b => (a -> b)) as bs))
 12 |       -> HVect1 bs
 13 | happly [] [] = ?h1 -- []
                ^^

[Mr-Andersen]

I tried another approach (see branch second), it led to both a warning and an error appear:

1/1: Building Main (src/Main.idr)
Warning: Unreachable clause: case block in happly bs as k xs

src/Main.idr:20:9--20:21
 16 |       -> HVect1 bs
 17 | happly [] =
 18 |     \case
 19 |         [] => ?hole1
 20 |         xs => ?hole2
              ^^^^^^^^^^^^

Error: While processing right hand side of happly. Can't solve constraint between: [] and zipWith (\a, b => a -> b) [] ?_.

src/Main.idr:19:9--19:11
 15 |       -> (1 _ : HVect1 (zipVect {k} (\a, b => (a -> b)) as bs))
 16 |       -> HVect1 bs
 17 | happly [] =
 18 |     \case
 19 |         [] => ?hole1
              ^^

[gallais]

zipWith matches on both of its arguments before returning [].

By matching on a value of type HVect1 as you've ensured that as = [] but you still need to reveal that bs = [] for the function to reduce.

[Mr-Andersen]

But they both have type Vect k Type. Can I make it more clear for the compiler?

[Mr-Andersen]

Does "status: expected behaviour" means, that this is not gonna be fixed?

[Mr-Andersen]

Oh, un-erasing {n : Nat} makes it ok to match on bs (even though it is erased): happly {bs=[]} [] [] = []. With little blood, it works, thanks

[gallais]

It's always going to be painful to pattern-match on values that are indexed by computations that do not quite reduce enough for your purposes. Alternatively you could have a different representation of the problem that does not require any computation to happen:

import Data.List.Quantifiers

HVect : List Type -> Type
HVect = All id

-- do we have this somewhere already? Can't remember
data Pointwise : (a -> b -> Type) -> List a -> List b -> Type where
  Nil : Pointwise f [] []
  (::) : {0 f : a -> b -> Type} -> f x y -> Pointwise f xs ys -> Pointwise f (x :: xs) (y :: ys)

infixr 1 ==>
(==>) : List Type -> List Type -> Type
(==>) = Pointwise (\a, b => (a -> b))

happly : HVect as -> as ==> bs -> HVect bs
happly [] [] = []
happly (x :: xs) (f :: fs) = f x :: happly xs fs

Advantageously this definition of HVect in terms of the more general All allows you to naturally express things like:

hsequence : Applicative f => All f as -> f (HVect as)
hsequence [] = pure []
hsequence (mx :: mxs) = [| mx :: hsequence mxs |]

[buzden]

Oh, un-erasing {n : Nat} makes it ok to match on bs (even though it is erased): happly {bs=[]} [] [] = []. With little blood, it works, thanks

By the way, you could match on k even it's erased (thanks to the match [] on the first explicit argument). It's unclear to me why having k not erased makes matching on bs valid, but having k erased (but still known to be 0) disallows matching on bs (of type Vect 0 Type).

[gallais]

It's unclear to me why having k not erased makes matching on bs valid, but having k erased (but still known to be 0) disallows matching on bs (of type Vect 0 Type).

I'm guessing it's something like https://github.com/idris-lang/Idris2/issues/1259#issuecomment-814258909

[buzden]

Yeah, but it means that the original example in this ticket is not an expected behaviour, since bs is actually expected to be unified with []; thus zipWith would be applied to [] as the third argument and thus reduced to []; and the original code would typecheck.

[gallais]

since bs is actually expected to be unified with [];

I don't think it is as there is no match forcing it to be.

Like we don't expect all proofs of a = a to be definitionally equal to Refl. You still need to match on it.