How do I fix the 'cannot decide' error in the opt function?

LittleLang.agda

module LittleLang where

open import Data.Bool
open import Data.Nat

data type : Set where
  tNat tBool : type

data exp : type → Set where
  nat  : ℕ → exp tNat
  plus : exp tNat → exp tNat → exp tNat
  bool : Bool → exp tBool
  and  : exp tBool → exp tBool → exp tBool

fromType : type → Set
fromType tNat  = ℕ
fromType tBool = Bool

eval : ∀ {t : type} → exp t → fromType t
eval (nat n)    = n
eval (plus n m) = eval n + eval m
eval (bool b)   = b
eval (and a b)  = eval a ∧ eval b

opt : ∀ {t : type} → exp t → exp t
opt (nat n) = nat n
opt (plus n m) with opt n | opt m
... | nat 0 | y     = y
... | x     | nat 0 = x
... | x     | y     = plus x y
opt (bool b) = bool b
opt (and a b) with opt a | opt b
... | bool true | y         = y
... | x         | bool true = x
... | x         | y         = and x y

Even though there's no way to construct a plus term with type exp Bool, the compiler says it cannot decide if there should be a case for the bool constructor. How do/Can I fix this?

If I make the appropriate changes to accomodate with eval n | eval m everything type checks fine, but the program is essentially being fully evaluated (which isn't what I want).

Thanks to @pigworker. I had to introduce a datatype to encode the types that LittleLang operates on and index exp by that.