transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥

[howtonotwin]

transpX clauses can be beat out by user-written _ clauses, leading to proof of ⊥

[jespercockx]

It's a map so the order really doesn't matter:

agda/src/full/Agda/TypeChecking/CompiledClause.hs

Line 41 in ea16c4c

, conBranches :: Map QName (WithArity c)

[andreasabel]

This can be reproduced immediately with Agda 2.6.3, but older versions of Agda 2.6 do not export PathP from Agda.Primitive.Cubical.

[andreasabel]

{-# OPTIONS -v tc.cc:15 #-} reveals this:

clauses before compilation
  onS¹ base = ⊤ 
  onS¹ (loop i) = ⊤ 
  onS¹ _ = ⊥

The constructed clauses are then generated (but not debug printed).
The case tree looks like this:

compiled clauses of  onS¹
  case 0 of
    Issue7033.D.base -> done[] Issue7033.⊤
    Issue7033.D.loop -> done[i] Issue7033.⊤
    Agda.Primitive.Cubical.primHComp -> done[{_}, {_}, {_}, _, _] Issue7033.⊥
    _ -> done[_] Issue7033.⊥

It seems that hcomp should maybe not be mapped to the empty type here. What should it be mapped to?

[howtonotwin]

Well, I'm not familiar with the Agda internals, but the generated clause looks fine to me (-v tc.def.fun.clauses:15):

onS¹ base = ⊤
onS¹ (loop i) = ⊤
onS¹ _ = ⊥
onS¹ (hcomp {.Agda.Primitive.lzero} {.D} {φ = φ} u a)
  = primComp (λ i .o → onS¹ (u i _)) (onS¹ a)

It's just that, when the case tree is made, the hcomp case is caught by the _ clause. The non-problematic definition

onS¹ : D → Set
onS¹ base     = ⊤
onS¹ (loop i) = ⊤
onS¹ other    = ⊥

produces the case tree

case 0 of
  Issue7033-1-none.D.base -> done[] Issue7033-1-none.⊤
  Issue7033-1-none.D.loop -> done[i] Issue7033-1-none.⊤
  Issue7033-1-none.D.other -> done[] Issue7033-1-none.⊥
  Agda.Primitive.Cubical.primHComp ->
    done[{_}, {_}, {_}, _, _]
      Agda.Primitive.Cubical.primComp
        {λ i -> lsuc lzero} {λ i -> Set}
        {Agda.Primitive.Cubical.primIMax @2 Agda.Primitive.Cubical.i0}
        (λ i -> λ o -> Issue7033-1-none.onS¹ (@3 @1 @0))
        (Issue7033-1-none.onS¹ @0)

I would think that last term is the correct one that should also appear in the case tree for the problematic version of onS¹.

[jespercockx]

Would it make sense to consider the generated hcomp clauses as coming first instead of last for the purpose of constructing the case tree?

[andreasabel]

Would it make sense to consider the generated hcomp clauses as coming first instead of last for the purpose of constructing the case tree?

This would probably fix the issue and we could go for this now.
Might have some negative impact on performance if the hcomp case is always tried first...

[jespercockx]

For the case tree it doesn't matter since it is just a switch on the constructor name, no? Or do we still go through all of the constructors linearly? In that case we could still force the hcomp constructor to come last, but before any catchall branches.

[andreasabel]

There is a statement in the code asking for adding hcomp clauses at the end:

agda/src/full/Agda/TypeChecking/Coverage/Cubical.hs

Line 1361 in ea16c4c

addClauses f [cl] -- Important: add at the end.

Unfortunately, direct blame history is truncated at 145dc62 due to code movement.
Tracing it manually, https://github.com/agda/agda/blame/d845567b76c0c5d963c7e19801acc63c3c85516a/src/full/Agda/TypeChecking/Coverage.hs#L1903 , gets us to the initial commit, fbc50e5, which already had the "Important: add at the end" comment.

[plt-amy]

The reason behind hcomp clauses having to come last, I assume, is a question of strictness. Since hcomp always looks like a Def, regardless of whether or not it's actually something you can match on (e.g. in higher inductive types), it's infeasible for an arbitrary function to tell, if they're splitting on a Def hcomp ..., whether that's actually an "hcomp-constructor", or whether it's just something unevaluated.

Placing the hcomp clauses after the constructor cases makes it so that the ordinary pattern-matching behaviour will force the split argument to head-normal form, so that if you actually did end up with a Def, you can be sure it's actually of the hcomp-constructor variety.

In that case we could still force the hcomp constructor to come last, but before any catchall branches.

This would work, but I'm not yet familiar enough with the coverage code to figure out how to do it. (This should also happen for transpX clauses.)