Not strictly positivite when using an equality proof inside a data type that has a forward declaration

Test.idr

%default total  

data Foo : Type
-- comment out the next line to have things type check.
data Bar : Foo -> Foo -> Type          
                                                                                                  
data Foo : Type where      
  MkFoo : Foo                                                                             
  
data Bar : Foo -> Foo -> Type where                                                       
  MkBar : {f : Foo} -> {prf : f = MkFoo} -> Bar f f