Agda-2.3.2.2: test/fail/ShouldBeASort.agda

-- This error never occurs.
module ShouldBeASort where

err = ShouldBeASort-Never-Occurs