Scone Creep Delicious when Scope Creep is not?

scone_creep.idr

data Creep = SomeCreep
data Scope a = SomeScope a
data Scone a = AScone a

data Taste a =
    Disgusting
  | Yucky
  | Edible
  | Yummy
  | Delicious

class Tasteable a where
  taste : Taste a

instance Tasteable Creep where
  taste = Edible

instance Tasteable a => Tasteable (Scone a) where
  taste = case taste of
            Delicious => Delicious
            Yummy => Delicious
            Edible => Yummy
            Yucky => Yucky
            Disgusting => Disgusting

instance Tasteable a => Tasteable (Scope a) where
  taste = case taste of
            Delicious => Edible
            Yummy => Yucky
            Edible => Disgusting
            Yucky => Disgusting
            Disgusting => Disgusting

data HasTaste : (a:Type) -> (t:Taste a) -> Type where
  -- Prove something is delicious by having the compiler taste it
  TryIt : Tasteable a => HasTaste a taste

-- Agree to eat something, but only if it can be proved Delicious
-- ahead of time.
eatThis : a -> HasTaste a Delicious -> String
eatThis _ _ = "Yum, that was Delicious!"

main : IO ()
main = do
  -- putStrLn $ eatThis SomeCreep TryIt -- won't compile
  -- putStrLn $ eatThis (AScone SomeCreep) TryIt -- won't compile
  -- putStrLn $ eatThis (SomeScope SomeCreep) TryIt -- *definitely* won't compile
  putStrLn $ eatThis (AScone (AScone SomeCreep)) TryIt -- compiles!

do not want to eat SomeCreep