Singletons/AtPattern.hs:0:0: Splicing declarations singletons [d| maybePlus :: Maybe Nat -> Maybe Nat maybePlus (Just n) = Just (plus (Succ Zero) n) maybePlus foo@Nothing = foo |] ======> Singletons/AtPattern.hs:(0,0)-(0,0) maybePlus :: Maybe Nat -> Maybe Nat maybePlus (Just n) = Just (plus (Succ Zero) n) maybePlus foo@Nothing = foo type instance MaybePlus (Just n) = Just (Plus (Succ Zero) n) type instance MaybePlus Nothing = Nothing type family MaybePlus (a :: Maybe Nat) :: Maybe Nat sMaybePlus :: forall (t :: Maybe Nat). Sing t -> Sing (MaybePlus t) sMaybePlus (SJust n) = SJust (sPlus (SSucc SZero) n) sMaybePlus foo@SNothing = foo