1 + 1 = 2?

onePlusOne.hs

-- {-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}



data Nil
data Cons x xs

class First list x | list -> x
instance First Nil Nil
instance First (Cons x more) x


data Z
data S n
data True'
data False'

class Eq' x y | x -> y
instance Eq' Z Z
instance (Eq' x y) => (Eq' (S x) (S y))

silly :: (Eq' (S Z) Z) => a
silly = undefined

verySerious :: Int
verySerious = undefined

oneEqualsOne :: (Eq' (S Z) (S Z)) => a
oneEqualsOne = undefined

class Plus x y z | x y -> z
instance Plus Z Z Z
instance Plus (S x) Z (S x)
instance Plus Z (S y) (S y)
instance Plus x y z => (Plus (S x) (S y) (S (S z)))


onePlusOneEqualsTwo :: (Plus (S Z) (S Z) (S (S Z))) => a
onePlusOneEqualsTwo = undefined