singletons-0.10.0: tests/compile-and-dump/Singletons/AtPattern.ghc76.template
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