Jonathan Cubides 7de9f2f0f3 Add new case for positivity checker: type cannot occur as arg of bound var (#2542) ... This PR fixes our positivity checker to support inductive definitions with type families as type parameters. This kind of ind. type is type-checked using the global flag `--new-type checker.` For example, the following definition is not allowed: ``` module Evil; type Evil (f : Type -> Type) := magic : f (Evil f) -> Evil f; ``` - Closes #2540		2023-11-30 15:03:54 +01:00
..
Negative.hs	Add new case for positivity checker: type cannot occur as arg of bound var (#2542)	2023-11-30 15:03:54 +01:00
NegativeNew.hs	Add new case for positivity checker: type cannot occur as arg of bound var (#2542)	2023-11-30 15:03:54 +01:00
Positive.hs	Negative tests for --new-typechecker (#2532)	2023-11-28 17:24:03 +00:00
PositiveNew.hs	Improve inference for --new-typechecker (#2524)	2023-11-28 16:43:14 +01:00