Problems with stdlib translation

[thiagofelicissimo]

When translating this file from the stdlib, I ran into a pattern of the form DefP used for HITs, which then fails as the translator does not support them. However, the file being translated does not use cubical features, and the function which causes a problem is the following, which does not appear to have nothing to do with HITs.

recompute : ∀ {a} {A : Set a} → Dec A → .A → A
recompute (yes x) _ = x
recompute (no ¬p) x = ⊥-elim (¬p x)

When looking at the case tree, we have the fragment (not showing everything, as it's too huge)

funCompiled     =
  case 2 of
    eta Relation.Nullary._because_ ->
      case 2 of
	Agda.Builtin.Bool.Bool.false ->
	  case 2 of
	    Relation.Nullary.Reflects.ofⁿ ->
	      done[{_}, {_}, ¬p, x]
		Data.Empty.Irrelevant.⊥-elim {@3} {@2} (@1 @0)
	    Agda.Primitive.Cubical.primHComp ->
	      done[{_}, {_}, {_}, {_}, {_}, _, _, _]
		Agda.Primitive.Cubical.primComp
		  {λ i -> @8} (λ i -> @7)
		  {Agda.Primitive.Cubical.primIMax @3 Agda.Primitive.Cubical.i0}
		  (λ i ->
		     λ o ->
		       Relation.Nullary.recompute
			 {@9} {@8}
			 (Relation.Nullary._because_
			    Agda.Builtin.Bool.Bool.false (@4 @1 @0))
			 (Agda.Primitive.Cubical.primTransp
			    {λ i -> @10} (λ i -> @9)
			    (Agda.Primitive.Cubical.primIMax
			       (Agda.Primitive.Cubical.primINeg
				  (Agda.Primitive.Cubical.primINeg @1))
			       Agda.Primitive.Cubical.i0)
			    @2))
		  (Relation.Nullary.recompute
		     {@7} {@6}
		     (Relation.Nullary._because_
			Agda.Builtin.Bool.Bool.false @1)
		     (Agda.Primitive.Cubical.primTransp
			{λ i -> @8} (λ i -> @7)
			(Agda.Primitive.Cubical.primIMax
			   (Agda.Primitive.Cubical.primINeg
			      (Agda.Primitive.Cubical.primINeg
				 Agda.Primitive.Cubical.i0))
			   Agda.Primitive.Cubical.i0)
			@0))

which is quite weird, as the branches using cubical primitives do not appear in the original definition. @jespercockx do you have an idea of what might be happening? Are those maybe inserted internally to discharge the branches with impossible indices? If so, does this mean that the cubical part of Agda is also used in the "standard" one?

[jespercockx]

These extra clauses are indeed inserted by the implementation of --cubical. Since you can import files that use --without-K from files that use --cubical, these extra clauses are also generated for all definitions in files that use --without-K. If you're not using --cubical anywhere then it should be safe to just ignore the clauses with DefP patterns.

[thiagofelicissimo]

Ah ok I see, thanks!