Module fails to type check after parametrising it by postulates

[bafain]

In the following Agda code, module M2 is obtained by parametrising module M1 by what it postulates.

{-# OPTIONS --cubical #-}
module Issue where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

module M1 where
  postulate A : Set; a a' b b' : A; α : a ≡ a'; β : b ≡ b'; p : a ≡ b

  p' l : a' ≡ b'
  p' = primTransp (λ j → α j ≡ β j) i0 p
  l  = λ i → primHComp (λ { j (i = i0) → α j ; j (i = i1) → β j }) (p i)

  -- SUCCEEDS:
  _ : p' ≡ l
  _ = λ _ → p'

module M2 (A : Set) (a a' b b' : A) (α : a ≡ a') (β : b ≡ b') (p : a ≡ b) where
  p' l : a' ≡ b'
  p' = primTransp (λ j → α j ≡ β j) i0 p
  l  = λ i → primHComp (λ { j (i = i0) → α j ; j (i = i1) → β j }) (p i)

  -- FAILS:
  -- _ : p' ≡ l
  -- _ = λ _ → p'
  -- 
  -- `transp` for `_≡_ {A} = PathP (λ _ → A)` computes in terms of
  -- `comp` for `λ _ → A` which computes in terms of (`hcomp` for `A`
  -- and) `transp` for `λ _ → A` which is not the identity in general.

Module M1 type checks but module M2 fails to type check and Agda (version 2.6.1-ab2cd05) makes the following complaint:

primTransp (λ i → A) i
(primPOr i0 (primIMax (primINeg i0) i0) (λ .o → p i0)
 (primPOr (primINeg i0) i0 (λ _ → α i) (λ _ → β i)) _)
[= primTransp (λ i → A) i (α i)]
!= α i of type A

Is this behaviour expected?

[nad]

I don't know, but postulates and variables are not treated in exactly the same way, because variables can be instantiated, whereas postulates cannot.

[Saizan]

When A is a postulate we assume transp is the identity, this works well for String, Int and such other builtins.

It also makes sense if you think of postulates as global axioms: a fibrant type in a closed context might as well have transp be the identity.

In practice I also use postulates to sketch something and then turn it into parameters later, so I agree this is a bit confusing.

Maybe only postulates connected to a builtin should behave this way?

[WolframKahl]

I'd say that postulates are parameters that just happen to be declared in a way that makes it impossible to actually supply them.

So it makes sense to make postulates otherwise behave like parameters.

[jespercockx]

@Saizan Are you still planning to fix this before the release? If not, please bump it to 2.6.3.