Agda-2.3.2.2: test/fail/Issue690.err
Issue690.agda:14,6-7 D is not strictly positive, because it occurs in the second argument to _≡_ in the type of the constructor abs in the definition of D.
Issue690.agda:14,6-7 D is not strictly positive, because it occurs in the second argument to _≡_ in the type of the constructor abs in the definition of D.