fork(2) download

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances #-}
 
main = return ()
 
data Nat = Z | S Nat
 
data Even (a :: Nat) :: * where
  ZeroEven :: Even Z
  NextEven :: Even n -> Even (S (S n))
 
type family   Add (n :: Nat) (m :: Nat) :: Nat
type instance Add Z m = m
type instance Add (S n) m = S (Add n m)
 
type family   Mult (n :: Nat) (m :: Nat) :: Nat
type instance Mult Z m = Z
type instance Mult (S n) m = Add (Mult n m) n
 
evenPlusEven :: Even n -> Even m -> Even (Add n m)
evenPlusEven ZeroEven m = m
evenPlusEven (NextEven n) m = NextEven (evenPlusEven n m)
 
evenTimesEven :: Even n -> Even m -> Even (Mult n m)
evenTimesEven ZeroEven m = ZeroEven
evenTimesEven (NextEven n) m = evenPlusEven (evenTimesEven n m) (evenPlusEven m m)

[1 of 1] Compiling Main             ( prog.hs, prog.o )

prog.hs:25:32: error:
    • Could not deduce: Add (Mult n1 m) (Add m m)
                        ~
                        Add (Add (Mult n1 m) n1) ('S n1)
      from the context: n ~ 'S ('S n1)
        bound by a pattern with constructor:
                   NextEven :: forall (n :: Nat). Even n -> Even ('S ('S n)),
                 in an equation for ‘evenTimesEven’
        at prog.hs:25:16-25
      Expected type: Even (Mult n m)
        Actual type: Even (Add (Mult n1 m) (Add m m))
      NB: ‘Add’ is a type function, and may not be injective
    • In the expression:
        evenPlusEven (evenTimesEven n m) (evenPlusEven m m)
      In an equation for ‘evenTimesEven’:
          evenTimesEven (NextEven n) m
            = evenPlusEven (evenTimesEven n m) (evenPlusEven m m)
    • Relevant bindings include
        m :: Even m (bound at prog.hs:25:28)
        n :: Even n1 (bound at prog.hs:25:25)
        evenTimesEven :: Even n -> Even m -> Even (Mult n m)
          (bound at prog.hs:24:1)

Standard output is empty