diff --git a/app/Main.hs b/app/Main.hs
index dff6df9..a90f3bb 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -10,6 +10,7 @@ import Text.Megaparsec
 import PrettyPrinter.Enum
 import PrettyPrinter.Type
 import PrettyPrinter.Function
+import PrettyPrinter.RosettaObject
 import Semantic.TypeChecker
 import Semantic.ExpressionChecker
 import Semantic.FunctionChecker
@@ -71,32 +72,32 @@ parseFile :: String -> Either (ParseErrorBundle Text Void) (Header, [RosettaObje
 parseFile plainText = parse rosettaParser "" (Text.pack plainText)
 
 -- |Converts a RosettaObject into a plain haskell string
-printObject :: RosettaObject -> String
-printObject (TypeObject t) = printType t
-printObject (FunctionObject f) = printFunction f
-printObject (EnumObject e) = printEnum e
+-- printObject :: CheckedRosettaObject -> String
+-- printObject (CheckedTypeObject t) = printType t
+-- printObject (CheckedFunctionObject f) = printFunction f
+-- printObject (CheckedEnumObject e) = printEnum e
 
 -- |Checks all the objects from a list
-checkObjects :: [(([Type], [Symbol]), (Header, [RosettaObject]))] -> [(Header, [Either [TypeCheckError] RosettaObject])]
+checkObjects :: [(([Type], [Symbol]), (Header, [RosettaObject]))] -> [(Header, [Either [TypeCheckError] CheckedRosettaObject])]
 checkObjects [] = []
 checkObjects (((definedTypes, definedSymbols), (header, objs)) : rest) = (header, checked) : checkObjects rest
     where
         checked = map (checkObject (definedTypes, definedSymbols)) objs
 
 -- |Checks the RosettaObject for type errors
-checkObject :: ([Type], [Symbol]) -> RosettaObject -> Either [TypeCheckError] RosettaObject
+checkObject :: ([Type], [Symbol]) -> RosettaObject -> Either [TypeCheckError] CheckedRosettaObject
 -- |Checks the type and attributes of a type
 checkObject (definedTypes, _) (TypeObject t) =
     case checkType definedTypes t of
         Left errors -> Left errors
-        Right typ -> Right $ TypeObject typ
+        Right typ -> Right $ CheckedTypeObject typ
 -- |If an enum parses, it cannot throw an error
-checkObject _ (EnumObject e) = Right (EnumObject e)
+checkObject _ (EnumObject e) = Right $ CheckedEnumObject e
 -- |Checks the function inputs, output and assignment
 checkObject (definedTypes, definedFunctions) (FunctionObject fun) =
     case checkFunction (definedTypes, defaultMap ++ definedFunctions) fun of
         Left errors -> Left errors
-        Right func -> Right $ FunctionObject func
+        Right func -> Right $ CheckedFunctionObject func
 
 -- |Adds new defined functions into the symbol table
 addNewFunctions :: ([Type], [Symbol]) -> [RosettaObject] -> Either [TypeCheckError] [Symbol]
@@ -140,5 +141,5 @@ parseFunction = do
     FunctionObject <$> functionParser
 
 -- |Generate a new haskell file based on the rosetta objects and header
-generateFile :: (Header, [RosettaObject]) -> IO ()
-generateFile (header, objects) = writeFile (haskellFileName $ namespace header) (printHeader header ++ concatMap printObject objects)
\ No newline at end of file
+generateFile :: (Header, [CheckedRosettaObject]) -> IO ()
+generateFile (header, objects) = writeFile (haskellFileName $ namespace header) (printHeader header ++ concatMap printRosettaObject objects)
\ No newline at end of file
diff --git a/src/Model/Function.hs b/src/Model/Function.hs
index c2fd00f..763a464 100644
--- a/src/Model/Function.hs
+++ b/src/Model/Function.hs
@@ -23,4 +23,5 @@ data ExplicitFunction =
     MakeExplicitFunction {
         sign :: FunctionSignature,
         explicitAssignment :: ExplicitExpression 
-    }
\ No newline at end of file
+    }
+    deriving Show
\ No newline at end of file
diff --git a/src/Model/RosettaObject.hs b/src/Model/RosettaObject.hs
index 95024e7..82bf078 100644
--- a/src/Model/RosettaObject.hs
+++ b/src/Model/RosettaObject.hs
@@ -9,4 +9,10 @@ data RosettaObject =
     EnumObject EnumType
     | TypeObject Type
     | FunctionObject Function
+    deriving Show
+
+data CheckedRosettaObject =
+    CheckedEnumObject EnumType
+    | CheckedTypeObject Type
+    | CheckedFunctionObject ExplicitFunction
     deriving Show
\ No newline at end of file
diff --git a/src/Model/Type.hs b/src/Model/Type.hs
index 2f067bc..e6559bd 100644
--- a/src/Model/Type.hs
+++ b/src/Model/Type.hs
@@ -45,12 +45,12 @@ data Expression = Variable String
 
 data ExplicitExpression = ExplicitEmpty
     | ExplicitVariable {name :: String, returnCoercion :: Coercion}
-    | Value {returnCoercion :: Coercion}
+    | Value {name :: String, returnCoercion :: Coercion}
     | ExplicitList [ExplicitExpression]
     | ExplicitParens ExplicitExpression
-    | ExplicitFunction {name :: String, args :: [Coercion], returnCoercion :: Coercion}
-    | ExplicitIfSimple {cond :: Coercion, returnCoercion :: Coercion}
-    | ExplicitIfEsle {cond :: Coercion, args :: [Coercion], returnCoercion :: Coercion}
+    | ExplicitFunction {name :: String, args :: [(ExplicitExpression, Coercion)], returnCoercion :: Coercion}
+    | ExplicitIfSimple {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
+    | ExplicitIfElse {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), block2 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
     deriving (Show)
 
 data TypeCoercion =
@@ -61,7 +61,12 @@ data TypeCoercion =
 
 data CardinalityCoercion =
     MakeCardinalityIdCoercion {toCardinality :: Cardinality}
-    | MakeCardinalityCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality, transformCardinality :: String}
+    | MakeListCardinalityCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
+    | MakeNothing2MaybeCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
+    | MakeNothing2ListCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
+    | MakeMaybe2ListCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
+    | MakeObject2MaybeCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
+    | MakeObject2ListCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality}
     deriving (Show)
 
 -- |Used to handle polymorphism in Rosetta
diff --git a/src/PrettyPrinter/Function.hs b/src/PrettyPrinter/Function.hs
index 44fd942..3115d56 100644
--- a/src/PrettyPrinter/Function.hs
+++ b/src/PrettyPrinter/Function.hs
@@ -11,60 +11,63 @@ import Model.Type
 -- show printStatementTree 
 
 -- |Converts a Function into a haskell valid String
-printFunction :: Function -> String
-printFunction f = show $ vcat [printFunctionSignature f, printFunctionBody f, emptyDoc]
+printFunction :: ExplicitFunction -> String
+printFunction f = show $ vcat [printFunctionSignature (sign f), printFunctionBody f, emptyDoc]
 
 -- |Converts the body of a Function into a haskell valid Doc
-printFunctionBody :: Function -> Doc a
-printFunctionBody (MakeFunction name _ inp out ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression inp (cardinality out) ex
-printExpression :: [TypeAttribute] -> Cardinality -> Expression -> Doc a
-printExpression inps c (Variable s) = printVariable varC c s
-    where 
-        varC = getVarCardinality inps s
-printExpression inps c (Int s) = printVariable (Bounds (1, 1)) c s
-printExpression inps c (Real s) = printVariable (Bounds (1, 1)) c s
-printExpression inps c (Boolean s) = printVariable (Bounds (1, 1)) c s
-printExpression inps c Empty = "empty"
-printExpression inps c (Parens ex) = "(" <> printExpression inps c ex <> ")"
-printExpression inps c (List ex) = list (map (printExpression inps c) ex)
-printExpression inps c (Function name ex) = pretty name <> tupled (map (printExpression inps c) ex) 
-printExpression inps c (PrefixExp name ex) = pretty name <+> printExpression inps c ex
-printExpression inps c (PostfixExp "exists" ex) = "isJust" <+> printExpression inps c ex
-printExpression inps c (PostfixExp "is absent" ex) = "isNothing" <+> printExpression inps c ex
-printExpression inps c (PostfixExp "single exists" ex) = "length" <+> printExpression inps c ex <+> "==" <+> "1"
-printExpression inps c (PostfixExp "multiple exists" ex) = "length" <+> printExpression inps c ex <+> ">" <+> "1" 
-printExpression inps c (PostfixExp "count" ex) = "length" <+> printExpression inps c ex
-printExpression inps c (PostfixExp name ex) = pretty name <+> printExpression inps c ex
+printFunctionBody :: ExplicitFunction -> Doc a
+printFunctionBody (MakeExplicitFunction (MakeFunctionSignature name _ inp out) ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression ex
+printExpression :: ExplicitExpression -> Doc a
+printExpression ExplicitEmpty = "[]" 
+printExpression (ExplicitVariable name coer) = printCoercion coer $ pretty name
+printExpression (Value s coer) = printCoercion coer $ pretty s
+printExpression (ExplicitParens ex) = "(" <> printExpression ex <> ")"
+printExpression (ExplicitList ex) = list (map printExpression ex)
+printExpression (ExplicitFunction "exists" args returnCoerce) = printCoercion returnCoerce "isJust" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printExpression (ExplicitFunction "is absent" args returnCoerce) = printCoercion returnCoerce "isNothing" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printExpression (ExplicitFunction "single exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> "1"
+printExpression (ExplicitFunction "multiple exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> ">" <+> "1" 
+printExpression (ExplicitFunction "count" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
 -- Equality expressions
 -- [a] a all = 
 -- any <>
-printExpression inps c (InfixExp "=" ex1 ex2) = printExpression inps c ex1 <+> "==" <+> printExpression inps c ex2
-printExpression inps c (InfixExp "<>" ex1 ex2) = printExpression inps c ex1 <+> "/=" <+> printExpression inps c ex2
-printExpression inps c (InfixExp "any =" ex1 ex2) = printExpression inps c ex2 <+> "`elem`" <+> printExpression inps c ex1
-printExpression inps c (InfixExp "all <>" ex1 ex2) = printExpression inps c ex2 <+> "`notElem`" <+> printExpression inps c ex1
---printExpression (InfixExp "all =" ex1 ex2) = "all (Eq)" <+> printExpression ex2 <+> printExpression ex1
-printExpression inps c (InfixExp "and" ex1 ex2) = printExpression inps c ex1 <+> "&&" <+> printExpression inps c ex2
-printExpression inps c (InfixExp "or" ex1 ex2) = printExpression inps c ex1 <+> "||" <+> printExpression inps c ex2
-printExpression inps c (InfixExp name ex1 ex2) = printExpression inps c ex1 <+> pretty name <+> printExpression inps c ex2
-printExpression inps (Bounds (0, 1)) (IfSimple cond ex) = "if" <+> printExpression inps (Bounds (1, 1)) cond <+> "then" <+> printExpression inps (Bounds (0, 1)) ex <+> "else" <+> "Nothing"
-printExpression inps c (IfSimple cond ex) = "if" <+> printExpression inps (Bounds (1, 1)) cond <+> "then" <+> printExpression inps c ex <+> "else" <+> "[]"
-printExpression inps c (IfElse cond ex1 ex2) = "if" <+> printExpression inps (Bounds (1, 1)) cond <+> "then" <+> printExpression inps c ex1 <+> "else" <+> printExpression inps c ex2
+printExpression (ExplicitFunction "=" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
+printExpression (ExplicitFunction "<>" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "/=" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
+printExpression (ExplicitFunction "any =" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`elem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printExpression (ExplicitFunction "all <>" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`notElem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printExpression (ExplicitFunction "all =" args returnCoerce) = "all (Eq)" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printExpression (ExplicitFunction "and" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "&&" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
+printExpression (ExplicitFunction "or" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "||" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
+printExpression (ExplicitFunction name args returnCoerce) = pretty name <+> tupled (zipWith printCoercion [c | (e,c) <- args] [printExpression e | (e, c) <- args])
+printExpression (ExplicitIfSimple cond thenBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> "Nothing"
+printExpression (ExplicitIfElse cond thenBlock elseBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> printCoercion (snd elseBlock) (printExpression $ fst elseBlock)
 
--- |Converts a variable into a maybe or list depending on necessity
-printVariable :: Cardinality -> Cardinality -> String -> Doc a
-printVariable (Bounds (1, 1)) (Bounds (1, 1)) s = pretty s
-printVariable (Bounds (1, 1)) (Bounds (0, 1)) s = "Just" <+> pretty s
-printVariable (Bounds (0, 1)) (Bounds (0, 1)) s = pretty s
-printVariable (Bounds (1, 1)) _ s = "[" <+> pretty s <+> "]"
-printVariable _ _ s = pretty s
+-- |Converts a coercion into a haskell string
+printCoercion :: Coercion -> Doc a -> Doc a
+printCoercion (MakeCoercion [] crd) d = printCardinalityCoercion crd d
+printCoercion (MakeCoercion (t: ts) crd) d = printTypeCoercion t <+> printCoercion (MakeCoercion ts crd) d
+
+printCardinalityCoercion :: CardinalityCoercion -> Doc a -> Doc a
+printCardinalityCoercion (MakeCardinalityIdCoercion _) d = d
+printCardinalityCoercion (MakeListCardinalityCoercion _ _) d = d
+printCardinalityCoercion (MakeNothing2MaybeCoercion _ _) d = "Nothing"
+printCardinalityCoercion (MakeNothing2ListCoercion _ _) d = "[]"
+printCardinalityCoercion (MakeMaybe2ListCoercion _ _) d = "maybeToList" <+> d
+printCardinalityCoercion (MakeObject2MaybeCoercion _ _) d = "Just" <+> d
+printCardinalityCoercion (MakeObject2ListCoercion _ _) d = "[" <> d <> "]"
+
+printTypeCoercion :: TypeCoercion -> Doc a
+printTypeCoercion (MakeIdCoercion _) = emptyDoc
+printTypeCoercion (MakeSuperCoercion _ _) = "super"
+printTypeCoercion (MakeTypeCoercion _ _ t) = pretty t
 
 -- |Converts a list of type attributes to a Doc with a list of variable names
 printVariableNames :: [TypeAttribute] -> Doc a
 printVariableNames vars = foldl (<+>) emptyDoc (map (pretty . attributeName) vars)
 
 -- |Converts a function into a haskell valid Doc representing the signature of the function
-printFunctionSignature :: Function -> Doc a
-printFunctionSignature (MakeFunction name description inputs output _) =
+printFunctionSignature :: FunctionSignature -> Doc a
+printFunctionSignature (MakeFunctionSignature name description inputs output) =
     printDescription description (pretty name <+> prettyPrintType (Prelude.map printCardinality (inputs ++ [output])))
 
 -- |Zips the signature with the needed characters ('::', '->')
diff --git a/src/PrettyPrinter/RosettaObject.hs b/src/PrettyPrinter/RosettaObject.hs
index e701b56..90ef728 100644
--- a/src/PrettyPrinter/RosettaObject.hs
+++ b/src/PrettyPrinter/RosettaObject.hs
@@ -6,7 +6,7 @@ import PrettyPrinter.Function
 import PrettyPrinter.Type
   
 -- |Converts a supported Rosetta object into a haskell valid String
-printRosettaObject :: RosettaObject -> String
-printRosettaObject (EnumObject a) = printEnum a
-printRosettaObject (TypeObject a) = printType a
-printRosettaObject (FunctionObject a) = printFunction a
\ No newline at end of file
+printRosettaObject :: CheckedRosettaObject -> String
+printRosettaObject (CheckedEnumObject a) = printEnum a
+printRosettaObject (CheckedTypeObject a) = printType a
+printRosettaObject (CheckedFunctionObject a) = printFunction a
\ No newline at end of file
diff --git a/src/Semantic/ExpressionChecker.hs b/src/Semantic/ExpressionChecker.hs
index 0630918..dcc1993 100644
--- a/src/Semantic/ExpressionChecker.hs
+++ b/src/Semantic/ExpressionChecker.hs
@@ -6,6 +6,7 @@ import Data.Maybe
 import Model.Type
 import Semantic.TypeChecker
 import Utils.Utils
+import Model.Type (CardinalityCoercion(MakeNothing2MaybeCoercion, MakeNothing2ListCoercion, MakeMaybe2ListCoercion, MakeObject2MaybeCoercion, MakeObject2ListCoercion))
   
 -- |A declared variable or function
 data Symbol = Var{
@@ -87,10 +88,10 @@ addVariables s ((MakeTypeAttribute name typ crd _)  : vars) = Var name (toHaskel
 -- |Checks the type of a given expression
 checkExpression :: [Symbol] -> Expression -> Either TypeCheckError ExplicitExpression  
 checkExpression symbolMap (Variable var) = findVarType var symbolMap 
-checkExpression _ (Int _) = Right $ Value $ MakeCoercion [MakeIdCoercion (BasicType "Integer")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
-checkExpression _ (Real _) = Right $ Value $ MakeCoercion [MakeIdCoercion (BasicType "Double")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
-checkExpression _ (Boolean _) = Right $ Value $ MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
-checkExpression _ Empty = Right $ Value $ MakeCoercion [MakeIdCoercion (BasicType "Empty")] (MakeCardinalityIdCoercion (Bounds (0, 0)))
+checkExpression _ (Int val) = Right $ Value val $ MakeCoercion [MakeIdCoercion (BasicType "Integer")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
+checkExpression _ (Real val) = Right $ Value val $ MakeCoercion [MakeIdCoercion (BasicType "Double")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
+checkExpression _ (Boolean val) = Right $ Value val $ MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1)))
+checkExpression _ Empty = Right $ Value "empty" $ MakeCoercion [MakeIdCoercion (BasicType "Empty")] (MakeCardinalityIdCoercion (Bounds (0, 0)))
 checkExpression symbolMap (Parens ex) = 
     case checkExpression symbolMap ex of
         Left err -> Left err
@@ -104,34 +105,34 @@ checkExpression symbolMap (InfixExp name ex1 ex2) = checkFunctionCall symbolMap
 checkExpression symbolMap (IfSimple cond ex) =
     case checkExpression symbolMap cond of
         Left err -> Left $ IfConditionNotBoolean $ show err
-        Right condType -> case coercionType conditionPreCoercion `isSubType` BasicType "Boolean" of
-            Left err -> Left $ IfConditionNotBoolean $ show cond ++ " :: " ++ show (coercionType conditionPreCoercion)
+        Right condType -> case returnCoercion condType `coercionIncluded` MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))) of
+            Left err -> Left $ IfConditionNotBoolean $ show cond ++ " :: " ++ show (coercionType $ typeCoercion $ returnCoercion condType)
             Right condCoerce -> 
                 case checkExpression symbolMap ex of
                     Left err -> Left err
-                    Right thenCoerce -> 
-                        Right $ ExplicitIfSimple 
-                            (MakeCoercion (condCoerce ++ conditionPreCoercion) (cardinalityCoercion $ returnCoercion condType)) (returnCoercion thenCoerce)
-            where
-                conditionPreCoercion = typeCoercion $ returnCoercion condType
+                    Right thenExp -> 
+                        Right $ ExplicitIfSimple (condType, condCoerce) 
+                        (thenExp, MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
+                         (MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp)) (returnCoercion thenExp)
+
 -- |Checks if the condition of the if statement is of type boolean, and then checks that both the then and else statements have the same type
 checkExpression symbolMap (IfElse cond ex1 ex2) =
     case checkExpression symbolMap cond of
         Left err -> Left $ IfConditionNotBoolean $ show err
-        Right condType -> 
-            case coercionType conditionPreCoercion `isSubType` BasicType "Boolean" of
-                Left err -> Left $ IfConditionNotBoolean $ show cond ++ " :: " ++ show (coercionType conditionPreCoercion)
-                Right condCoerce -> 
-                    case checkExpression symbolMap ex1 of
+        Right condType -> case returnCoercion condType `coercionIncluded` MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))) of
+            Left err -> Left $ IfConditionNotBoolean $ show cond ++ " :: " ++ show (coercionType $ typeCoercion $ returnCoercion condType)
+            Right condCoerce -> 
+                case checkExpression symbolMap ex1 of
+                    Left err -> Left $ ErrorInsideFunction $ show err
+                    Right thenExp -> case checkExpression symbolMap ex2 of
                         Left err -> Left $ ErrorInsideFunction $ show err
-                        Right ex1Checked -> case checkExpression symbolMap ex2 of
-                            Left err -> Left $ ErrorInsideFunction $ show err
-                            Right ex2Checked -> Right $ ExplicitIfEsle 
-                                (MakeCoercion (condCoerce ++ conditionPreCoercion) (cardinalityCoercion $ returnCoercion condType)) 
-                                (returnCoercion ex1Checked : [returnCoercion ex2Checked]) (returnCoercion ex1Checked)
-                            --(typeMatch ex1Type ex2Type, smallestBound ex1Card ex2Type)
-            where
-                conditionPreCoercion = typeCoercion $ returnCoercion condType
+                        Right elseExp -> 
+                            Right $ ExplicitIfElse (condType, condCoerce) 
+                            (thenExp, MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
+                             (MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp))
+                            (elseExp, MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion elseExp]
+                             (MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion elseExp)) (returnCoercion thenExp)
+                        --(typeMatch ex1Type ex2Type, smallestBound ex1Card ex2Type)
                 
 
 -- |TODO Handle nested lists and lists with parens
@@ -168,7 +169,7 @@ checkFunctionCall :: [Symbol] -> String -> [Either TypeCheckError ExplicitExpres
 checkFunctionCall [] fun args = Left $ UndefinedFunction $ "Undefined function: \"" ++ fun ++ "\" [" ++ show (rights args) ++ "]"
 checkFunctionCall ((Func n a r):symbolMap) name args
     | length (rights args) /= length args = Left $ ErrorInsideFunction (name ++ ": " ++ show args ++ show (lefts args))
-    | name == n && all isRight coerce = Right $ ExplicitFunction name (rights coerce) (MakeCoercion [MakeIdCoercion (fst r)] (MakeCardinalityIdCoercion (snd r))) 
+    | name == n && all isRight coerce = Right $ ExplicitFunction name (zip (rights args) (rights coerce)) (MakeCoercion [MakeIdCoercion (fst r)] (MakeCardinalityIdCoercion (snd r))) 
     | otherwise = checkFunctionCall symbolMap name args
     where 
         argCoerce = map returnCoercion (rights args)
@@ -227,19 +228,24 @@ isSubType x y
 -- |Checks whether the first cardinality is included into the second one 
 cardinalityIncluded :: Cardinality -> Cardinality -> Either TypeCheckError CardinalityCoercion
 -- |Special Cases
-cardinalityIncluded (Bounds (0, 0)) (Bounds (0, 1)) = Right $ MakeCardinalityCoercion (Bounds (0, 0)) (Bounds (0, 1)) "Nothing"
-cardinalityIncluded (Bounds (0, 0)) (OneBound 0) = Right $ MakeCardinalityCoercion (Bounds (0, 0)) (OneBound 0) "[]"
-cardinalityIncluded (Bounds (0, 1)) (OneBound 0) = Right $ MakeCardinalityCoercion (Bounds (0, 1)) (OneBound 0) "[Just]"
-cardinalityIncluded (Bounds (1, 1)) (Bounds (0, 1)) = Right $ MakeCardinalityCoercion (Bounds (0, 1)) (Bounds (0, 1)) "Just"
-cardinalityIncluded (Bounds (1, 1)) (OneBound 1) = Right $ MakeCardinalityCoercion (Bounds (0, 1)) (OneBound 1) "[]"
+-- |Transform nothing into a maybe
+cardinalityIncluded (Bounds (0, 0)) (Bounds (0, 1)) = Right $ MakeNothing2MaybeCoercion (Bounds (0, 0)) (Bounds (0, 1))
+-- |Transform nothing into a list
+cardinalityIncluded (Bounds (0, 0)) (OneBound 0) = Right $ MakeNothing2ListCoercion (Bounds (0, 0)) (OneBound 0)
+-- |Transform maybe into list
+cardinalityIncluded (Bounds (0, 1)) (OneBound 0) = Right $ MakeMaybe2ListCoercion (Bounds (0, 1)) (OneBound 0)
+-- |Transform object into maybe
+cardinalityIncluded (Bounds (1, 1)) (Bounds (0, 1)) = Right $ MakeObject2MaybeCoercion (Bounds (0, 1)) (Bounds (0, 1))
+-- |Transform object into list
+cardinalityIncluded (Bounds (1, 1)) (OneBound 1) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1)
 -- |General
 cardinalityIncluded (OneBound x) (OneBound y)
-    | x >= y = Right $ MakeCardinalityCoercion (OneBound x) (OneBound y) "id"
+    | x >= y = Right $ MakeListCardinalityCoercion (OneBound x) (OneBound y)
     | otherwise = Left $ CardinalityMismatch (OneBound x) (OneBound y)
 cardinalityIncluded (Bounds (x1, y1)) (OneBound y)
-    | x1 >= y = Right $ MakeCardinalityCoercion (Bounds (x1, y1)) (OneBound y) "id"
+    | x1 >= y = Right $ MakeListCardinalityCoercion (Bounds (x1, y1)) (OneBound y)
     | otherwise = Left $ CardinalityMismatch (Bounds (x1, y1)) (OneBound y)
 cardinalityIncluded (OneBound x) (Bounds (x2, y2)) = Left $ CardinalityMismatch (OneBound x) (Bounds (x2, y2))
 cardinalityIncluded (Bounds (x1, x2)) (Bounds (y1, y2))
-    | x1 >= y1 && x2 <= y2 = Right $ MakeCardinalityCoercion (Bounds (x1, x2)) (Bounds (y1, y2)) "id"
+    | x1 >= y1 && x2 <= y2 = Right $ MakeListCardinalityCoercion (Bounds (x1, x2)) (Bounds (y1, y2))
     | otherwise = Left $ CardinalityMismatch (Bounds (x1, x2)) (Bounds (y1, y2))