Unexpectedly accepted proof in Idris 0.9.19

test.idr

-- This is a reduction of code that I wrote last night.
-- I can use this code to produce a `Void`.

-- Because I'm new to Idris I may have simply misinterpreted
-- what's going on here, so I've tried to specify my
-- understanding in comments.

%default total

data Color = Red | Blue

-- An object can either be unfinished, or painted a color.
data Paint : Type where
  NoPaint : Paint
  Painted : Color -> Paint

-- A buyer will either take anything offered, or only objects painted a certain
-- color.
data Preference : Type where
  Anything : Preference
  LikesColor : Color -> Preference

-- Proof that buyer's preference has been met.
data PreferenceMet : Paint -> Preference -> Type where
  -- A buyer that accepts `Anything` will take an item without
  -- paint.
  Flexible : PreferenceMet NoPaint Anything
  -- A buyer with a particular preference will accept an object
  -- painted the same color.
  RightColor : PreferenceMet (Painted c) (LikesColor c)

  -- The type below, added by accident, allows for a counterexample
  -- in `wantsColor`.  It effectively states "an object with no paint
  -- will be accepted regardless of buyer preference."
  Break : PreferenceMet NoPaint _

-- Proof that a buyer who wants a certain color will not accept `NoPaint`.
-- i.e. there does not exist a color `c` such that `NoPaint` will satisfy
-- a preference for `c`.
wantsColor : Not (c ** PreferenceMet NoPaint (LikesColor c))
wantsColor (x ** Flexible) impossible
  -- This is accepted as total.
  -- And yet other constructors of the type *are* possible!

-- Counterexample for `wantsColor`.
counterWantsColor : Void
counterWantsColor = wantsColor (Red ** Break)

-- Different phrasing, same proof.  i.e. For all colors `c`, `NoPaint` will
-- not satisfy a preference for `c`.
wantsColor' : (c : Color) -> Not (PreferenceMet NoPaint (LikesColor c))
wantsColor' c Flexible impossible
  -- Same deal.

-- Counterexample for rephrasing.
counterWantsColor' : Void
counterWantsColor' = wantsColor' Red Break