G. Allais

FFS windows

The test suite has examples with `depends`. Are these not satisfactory?

Build error aside, I don't understand the patch: is it just moving an alternative around? Why should that make any difference in the absence of `commit`?

We discussed it with @edwinb last Thursday and agreed we should probably not have that extra syntax.

Minimised: ``` module Model import public Data.Bits %default total public export interface Bits ty => VerifiedBits ty where verify : (v : ty) -> v .&. v = v public...

`Fix` is not strictly positive (because we can't guarantee that `f` is) so it should be rejected.

Boom: ```idris %default total data Fix : (Type -> Type) -> Type where MkFix : f (Fix f) -> Fix f F : Type F = Fix Not yesF :...

Here's my understanding: When we check the type of `MkFix`, the first thing we encounter is a Pi-type binding `{0 f : Type -> Type}`. This argument is fine so...

A variant that's not relying on `Erased`: we drop the arguments to a type constructor that are in parameter positions by considering these are safe positive positions. That's what allows...

And here's a third one: it's not because an argument to a type constructor is a parameter that this parameter is used strictly positively in the definition of the type...