Agda-2.3.2.2: test/fail/Issue280.err
Issue280.agda:8,19-26 Recursive telescope in left hand side: (M : M c → Set) (c : M c) when checking that the pattern model c has type PreModel C M C
Issue280.agda:8,19-26 Recursive telescope in left hand side: (M : M c → Set) (c : M c) when checking that the pattern model c has type PreModel C M C