The "Could not generate equivalence" warning is not always emitted

[nad]

Now you can get a warning about how a certain definition by pattern matching "will not compute on transports by a path":

{-# OPTIONS --cubical #-}

data I : Set where
  i : I

data D : I → Set where
  c : D i

f : ∀ x → D x → D x
f i c = c

Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: UnsupportedYet Injectivity
                           position:    0
                           type:        I
                           datatype:    I
                           parameters: 
                           indices:    
                           constructor: i
when checking the definition of f

However, I don't get this warning if I define the code above in a module that uses --without-K and import and use it in a module that uses --cubical. Perhaps it would make sense to emit this warning more often. For instance, it could be emitted at most once per module that uses --cubical or --erased-cubical, at the first use of a problematic definition that was imported from a module that uses --without-K.

[nad]

Now that we have the new option --cubical-compatible it might make sense to revisit this issue. I suggest that the warning should (by default) be emitted when --cubical-compatible is used, and that the warning should be turned off in the standard library's .agda-lib file.