diff --git a/src/Model/Function.hs b/src/Model/Function.hs
index bba703e..c2fd00f 100644
--- a/src/Model/Function.hs
+++ b/src/Model/Function.hs
@@ -1,14 +1,26 @@
 module Model.Function where
 
-import Model.Type (TypeAttribute, Expression)
+import Model.Type (TypeAttribute, Expression, ExplicitExpression)
   
--- |The representation of a Rosetta function type
-data Function = 
-    MakeFunction {
+data FunctionSignature = 
+    MakeFunctionSignature {
         functionName :: String,
         functionDescription :: Maybe String,
         inputParameters :: [TypeAttribute],
-        outputParameter :: TypeAttribute,
+        outputParameter :: TypeAttribute
+    }
+    deriving (Show)
+
+-- |The representation of a Rosetta function type
+data Function = 
+    MakeFunction {
+        signature :: FunctionSignature,
         assignment :: Expression
     }
-    deriving (Show)
\ No newline at end of file
+    deriving (Show)
+
+data ExplicitFunction = 
+    MakeExplicitFunction {
+        sign :: FunctionSignature,
+        explicitAssignment :: ExplicitExpression 
+    }
\ No newline at end of file
diff --git a/src/Model/Type.hs b/src/Model/Type.hs
index 9fd117b..2f067bc 100644
--- a/src/Model/Type.hs
+++ b/src/Model/Type.hs
@@ -1,5 +1,4 @@
 module Model.Type where
-
 -- |The representation of a Rosetta data type
 data Type = MakeType {
         typeName :: String,
@@ -14,9 +13,9 @@ data Type = MakeType {
     deriving (Show)
 
 instance Eq Type where
-    (==) (MakeType name _ _ _ _) (MakeType name2 _ _ _ _) 
+    (==) (MakeType name _ _ _ _) (MakeType name2 _ _ _ _)
         | name == name2 = True
-        | otherwise = False 
+        | otherwise = False
     (==) (BasicType name) (BasicType name2)
         | name == name2 = True
         | otherwise = False
@@ -27,7 +26,7 @@ data Condition = MakeCondition {
     conditionDescription :: Maybe String,
     expressionExpression :: Expression
 } deriving (Show)
-     
+
 -- |The representation of an expression
 data Expression = Variable String
     | Int String
@@ -44,6 +43,31 @@ data Expression = Variable String
     | IfElse Expression Expression Expression
     deriving (Eq, Show)
 
+data ExplicitExpression = ExplicitEmpty
+    | ExplicitVariable {name :: String, returnCoercion :: Coercion}
+    | Value {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}
+    deriving (Show)
+
+data TypeCoercion =
+    MakeIdCoercion {toType :: Type}
+    | MakeSuperCoercion {fromType :: Type, toType :: Type}
+    | MakeTypeCoercion {fromType :: Type, toType :: Type, transformType :: String}
+    deriving (Show)
+
+data CardinalityCoercion =
+    MakeCardinalityIdCoercion {toCardinality :: Cardinality}
+    | MakeCardinalityCoercion {fromCardinality :: Cardinality, toCardinality :: Cardinality, transformCardinality :: String}
+    deriving (Show)
+
+-- |Used to handle polymorphism in Rosetta
+data Coercion = MakeCoercion {typeCoercion :: [TypeCoercion], cardinalityCoercion :: CardinalityCoercion} deriving(Show)
+
+
 -- |The representation of an attribute of a data type
 data TypeAttribute = MakeTypeAttribute {
     attributeName :: String,
@@ -53,27 +77,22 @@ data TypeAttribute = MakeTypeAttribute {
 } deriving (Show)
 
 -- |The representation of cardinality
-data Cardinality = 
+data Cardinality =
     -- |The cardinality between two bounds (ex. 2 - 5)
   Bounds (Integer, Integer)
     -- |The cardinality starting from one bound until infinity (ex. 5 - *)
   | OneBound Integer
-    -- |The cardinality of no bounds (ex. * - *)
-  | NoBounds 
   deriving Show
-  
+
 instance Eq Cardinality where
     (==) (Bounds (x1, x2)) (Bounds (y1, y2))
         | x1 == y1 && x2 == y2 = True
         | otherwise = False
     (==) (OneBound x) (OneBound y) = x == y
-    (==) NoBounds NoBounds = True
     (==) _ _ = False
 
 -- |Function to create the smallest cardinality that includes two others
 smallestBound  :: Cardinality -> Cardinality -> Cardinality
-smallestBound NoBounds _ = NoBounds
-smallestBound _ NoBounds = NoBounds
 smallestBound (OneBound x) (OneBound y) = OneBound $ min x y
 smallestBound (OneBound x) (Bounds (y, _)) = smallestBound (OneBound x) (OneBound y)
 smallestBound (Bounds (x, _)) (OneBound y) = smallestBound (OneBound x) (OneBound y)
@@ -83,53 +102,34 @@ smallestBound (Bounds (x1, x2)) (Bounds (y1, y2)) = Bounds (min x1 y1, max x2 y2
 addBounds :: Cardinality -> Cardinality -> Cardinality
 addBounds (Bounds (x1, x2)) (Bounds (y1, y2)) = Bounds (x1 + y1, x2 + y2)
 addBounds (Bounds (x1, _)) (OneBound y1) = OneBound (x1 + y1)
-addBounds (Bounds (x1, _)) NoBounds = OneBound x1
 addBounds (OneBound x1) (Bounds (y1, y2)) = addBounds (Bounds (y1, y2)) (OneBound x1)
 addBounds (OneBound x1) (OneBound y1) = OneBound (x1 + y1)
-addBounds (OneBound x1) NoBounds = OneBound x1
-addBounds NoBounds (Bounds (y1, y2)) = addBounds (Bounds (y1, y2)) NoBounds
-addBounds NoBounds (OneBound y1) = addBounds (OneBound y1) NoBounds
-addBounds NoBounds NoBounds = NoBounds 
-    
+
 -- |Custom operator for adding cardinalities
 infixl 5 .+
 (.+) :: Cardinality -> Cardinality -> Cardinality
 (.+) = addBounds
-  
+
 typeAndCardinality :: TypeAttribute -> (Type, Cardinality)
 typeAndCardinality (MakeTypeAttribute _ typ crd _) = (typ, crd)
 
-    
--- |Checks whether the first argument is a subtype of the second argument
-isSubType :: Type -> Type -> Bool
-isSubType (BasicType "Integer") (BasicType "Double") = True
-isSubType _ (BasicType "Object") = True
-isSubType _ (BasicType "Any") = False
-isSubType (BasicType x) y 
-    | x == typeName y = True
-    | otherwise = False
-isSubType x y 
-    | typeName x == typeName y = True
-    | otherwise = isSubType (superType x) y
-    
--- |Checks whether the first cardinality is included into the second one 
-cardinalityIncluded :: Cardinality -> Cardinality -> Bool
-cardinalityIncluded _ NoBounds = True
-cardinalityIncluded NoBounds _ = False
-cardinalityIncluded (OneBound x) (OneBound y)
-    | x >= y = True
-    | otherwise = False
-cardinalityIncluded (Bounds (x1, _)) (OneBound y)
-    | x1 >= y = True
-    | otherwise = False
-cardinalityIncluded (OneBound _) (Bounds (_, _)) = False
-cardinalityIncluded (Bounds (x1, x2)) (Bounds (y1, y2))
-    | x1 >= y1 && x2 <= y2 = True
-    | otherwise = False
-
 toHaskell :: Type -> Type
 toHaskell a
     | typeName a == "int" = BasicType "Integer"
     | typeName a == "boolean" = BasicType "Boolean"
     | typeName a == "real" = BasicType "Double"
-    | otherwise = a
\ No newline at end of file
+    | otherwise = a
+
+coercionType :: [TypeCoercion] -> Type
+coercionType [] = BasicType "Empty"
+coercionType [x] = toType x 
+coercionType (x:rst) = coercionType rst
+
+-- |Gets the final cardinality from a list of coercions
+coercionCardinality :: [CardinalityCoercion] -> Cardinality
+coercionCardinality [] = OneBound 0
+coercionCardinality [x] = toCardinality x
+coercionCardinality (x:rst) = coercionCardinality rst
+
+createCoercion :: (Type, Cardinality) -> Coercion
+createCoercion (t, c) = MakeCoercion [MakeIdCoercion t] (MakeCardinalityIdCoercion c)
\ No newline at end of file
diff --git a/src/Parser/Function.hs b/src/Parser/Function.hs
index 6cf5b1d..808d2d1 100644
--- a/src/Parser/Function.hs
+++ b/src/Parser/Function.hs
@@ -20,7 +20,7 @@ functionParser =
         fDescription <- optional descriptionParser
         fInput <- inputAttributesParser
         fOutput <- outputAttributeParser
-        MakeFunction fName fDescription fInput fOutput <$> assignmentParser
+        MakeFunction (MakeFunctionSignature fName fDescription fInput fOutput) <$> assignmentParser
 
 -- |Parses the output assignment statement from a function in Rosetta into an Expression
 assignmentParser :: Parser Expression
diff --git a/src/Parser/Type.hs b/src/Parser/Type.hs
index 583133b..b6dada3 100644
--- a/src/Parser/Type.hs
+++ b/src/Parser/Type.hs
@@ -44,7 +44,7 @@ typeAttributeParser =
 
 -- |Parses the cardinality of a type attribute in Rosetta into a Cardinality
 cardinalityParser :: Parser Cardinality
-cardinalityParser = try parseBounded <|> try parseSemiBounded <|> try parseUnbounded
+cardinalityParser = try parseBounded <|> try parseSemiBounded
 
 -- |Parser the condition of a type attribute in Rosetta into a Condition
 conditionParser :: Parser Condition 
@@ -74,13 +74,6 @@ parseSemiBounded =
         low <- lexeme $ many digitChar
         _ <- lexeme $ string "..*)"
         return $ OneBound $ read low
-        
--- |Parses an unbounded cardinality statement in Rosetta into a Cardinality
-parseUnbounded :: Parser Cardinality
-parseUnbounded = 
-    do
-        _ <- lexeme $ string "(*..*)"
-        return NoBounds
 
 -- |Parses the name of a type in Rosetta into a String
 typeNameParser :: Parser String
diff --git a/src/PrettyPrinter/Type.hs b/src/PrettyPrinter/Type.hs
index c017c2b..0e16b42 100644
--- a/src/PrettyPrinter/Type.hs
+++ b/src/PrettyPrinter/Type.hs
@@ -37,7 +37,6 @@ printCardinality (MakeTypeAttribute _ typ (Bounds (x, y)) _)
     | x == 0 && y == 1 = "Maybe" <+> pretty (typeName typ)
     | x == 1 && y == 1 = pretty (typeName typ)
     | otherwise = "[" <> pretty (typeName typ) <> "]"
-printCardinality (MakeTypeAttribute _ typ NoBounds _) = "[" <> pretty (typeName typ) <> "]"
 printCardinality (MakeTypeAttribute _ typ (OneBound _) _) = "[" <> pretty (typeName typ) <> "]"
 
 printCondition :: Condition -> Doc a
diff --git a/src/Semantic/ExpressionChecker.hs b/src/Semantic/ExpressionChecker.hs
index 9d66773..0630918 100644
--- a/src/Semantic/ExpressionChecker.hs
+++ b/src/Semantic/ExpressionChecker.hs
@@ -36,21 +36,21 @@ defaultMap = [
   Func "and" [(BasicType "Boolean", Bounds (1, 1)), (BasicType "Boolean", Bounds (1, 1))] (BasicType "Boolean", Bounds (1, 1)),
   Func "exists" [(BasicType "Any", Bounds (0, 1))] (BasicType "Boolean", Bounds(1, 1)),
   Func "is absent" [(BasicType "Any", Bounds (0, 1))] (BasicType "Boolean", Bounds (1, 1)),
-  Func "single exists" [(BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds (1, 1)),
-  Func "multiple exists" [(BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds (1, 1)),
-  Func "contains" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds (1, 1)),
-  Func "disjoint" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds (1, 1)),
+  Func "single exists" [(BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds (1, 1)),
+  Func "multiple exists" [(BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds (1, 1)),
+  Func "contains" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds (1, 1)),
+  Func "disjoint" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds (1, 1)),
   
-  Func "=" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func ">=" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func "<=" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func "<>" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func ">" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func "<" [(BasicType "Any", NoBounds), (BasicType "Any", NoBounds)] (BasicType "Boolean", Bounds(1, 1)),
-  Func "all =" [(BasicType "Any", NoBounds), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
-  Func "all <>" [(BasicType "Any", NoBounds), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
-  Func "any =" [(BasicType "Any", NoBounds), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
-  Func "any <>" [(BasicType "Any", NoBounds), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
+  Func "=" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func ">=" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func "<=" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func "<>" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func ">" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func "<" [(BasicType "Any", OneBound 0), (BasicType "Any", OneBound 0)] (BasicType "Boolean", Bounds(1, 1)),
+  Func "all =" [(BasicType "Any", OneBound 0), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
+  Func "all <>" [(BasicType "Any", OneBound 0), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
+  Func "any =" [(BasicType "Any", OneBound 0), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
+  Func "any <>" [(BasicType "Any", OneBound 0), (BasicType "Any", Bounds(1, 1))] (BasicType "Boolean", Bounds(1, 1)),
   
   Func "+" [(BasicType "Integer", Bounds (1, 1)), (BasicType "Integer", Bounds (1, 1))] (BasicType "Integer", Bounds (1, 1)),
   Func "+" [(BasicType "Double", Bounds (1, 1)), (BasicType "Double", Bounds (1, 1))] (BasicType "Double", Bounds (1, 1)),
@@ -63,20 +63,21 @@ defaultMap = [
   Func "^" [(BasicType "Integer", Bounds (1, 1)), (BasicType "Integer", Bounds (1, 1))] (BasicType "Integer", Bounds (1, 1)),
   Func "^" [(BasicType "Double", Bounds (1, 1)), (BasicType "Double", Bounds (1, 1))] (BasicType "Double", Bounds (1, 1)),
   
-  Func "count" [(BasicType "Any", NoBounds)] (BasicType "Integer", Bounds (1, 1))
+  Func "count" [(BasicType "Any", OneBound 0)] (BasicType "Integer", Bounds (1, 1))
   ]
 
 -- |Checks whether a function is valid (inputs, outputs are of valid type and all variables are defined) and adds it to the symbol table
 addFunction :: ([Type], [Symbol]) -> Function -> Either [TypeCheckError] [Symbol]
-addFunction (definedTypes, definedSymbols) (MakeFunction name _ inps out _)
-    | null (lefts checkedInputs) && isRight checkedOutput = if name `elem` map funcName definedSymbols
-        then Left [MultipleDeclarations name]
-        else Right $ Func name (map typeAndCardinality (rights checkedInputs)) (attributeType $ fromRightUnsafe checkedOutput, Model.Type.cardinality out) : definedSymbols
-    | isLeft checkedOutput = Left [fromLeftUnsafe checkedOutput]
-    | otherwise = Left $  lefts checkedInputs 
+addFunction (definedTypes, definedSymbols) (MakeFunction (MakeFunctionSignature name _ inps out) _) =
+    case head $ checkAttributes definedTypes [out] of
+        Left err -> Left [err]
+        Right checkedOutput -> if null (lefts checkedInputs)
+            then if name `elem` map funcName definedSymbols
+                then Left [MultipleDeclarations name]
+                else Right $ Func name (map typeAndCardinality (rights checkedInputs)) (attributeType checkedOutput, Model.Type.cardinality out) : definedSymbols
+            else Left $ lefts checkedInputs
     where 
         checkedInputs = checkAttributes definedTypes inps
-        checkedOutput = head $ checkAttributes definedTypes [out]
         
 -- |Adds a newly defined variable to the symbol table
 addVariables :: [Symbol] -> [TypeAttribute] -> [Symbol]
@@ -84,76 +85,107 @@ addVariables s [] = s
 addVariables s ((MakeTypeAttribute name typ crd _)  : vars) = Var name (toHaskell typ) crd : addVariables s vars
         
 -- |Checks the type of a given expression
-checkExpression :: [Symbol] -> Expression -> Either TypeCheckError (Type, Cardinality)
-checkExpression symbolMap (Variable var) = findVarType var symbolMap
-checkExpression _ (Int _) = Right (BasicType "Integer", Bounds (1, 1))
-checkExpression _ (Real _) = Right (BasicType "Double", Bounds (1, 1))
-checkExpression _ (Boolean _) = Right (BasicType "Boolean", Bounds (1, 1))
-checkExpression _ Empty = Right (BasicType "Empty", Bounds (0, 0))
-checkExpression symbolMap (Parens ex) = checkExpression symbolMap ex
+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 symbolMap (Parens ex) = 
+    case checkExpression symbolMap ex of
+        Left err -> Left err
+        Right exp -> Right $ ExplicitParens exp
 checkExpression symbolMap (List lst) = checkList symbolMap lst 
 checkExpression symbolMap (PrefixExp name ex) = checkFunctionCall symbolMap name [checkExpression symbolMap ex]
 checkExpression symbolMap (Function name exps) = checkFunctionCall symbolMap name (map (checkExpression symbolMap) exps)
 checkExpression symbolMap (PostfixExp name ex) = checkFunctionCall symbolMap name [checkExpression symbolMap ex]
 checkExpression symbolMap (InfixExp name ex1 ex2) = checkFunctionCall symbolMap name (checkExpression symbolMap ex1: [checkExpression symbolMap ex2])
 -- |Checks if the condition of an if expression is of type boolean, and then checks the expression of the then statement
-checkExpression symbolMap (IfSimple cond ex)
-    | isRight condType && isSubType (fst $ fromRightUnsafe condType) (BasicType "Boolean") && snd (fromRightUnsafe condType) == Bounds (1, 1) = 
-        case checkedExp of
-            Right (typ, Bounds(_, x)) -> Right (typ, Bounds(0, x))
-            Right x -> Right x
-            Left err -> Left err
-    | otherwise = Left $ IfConditionNotBoolean $ show condType
-    where 
-        condType = checkExpression symbolMap cond
-        checkedExp = checkExpression symbolMap ex
+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 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
 -- |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)
-    | isLeft condType || not (isSubType (fst $ fromRightUnsafe condType) (BasicType "Boolean") && snd (fromRightUnsafe condType) == Bounds (1, 1)) = Left $ IfConditionNotBoolean $ show cond ++ " :: " ++ show condType
-    | otherwise = case checkExpression symbolMap ex1 of
-        Left err -> Left $ ErrorInsideFunction $ show err
-        Right ex1Type -> case checkExpression symbolMap ex2 of
-            Left err -> Left $ ErrorInsideFunction $ show err
-            Right ex2Type -> Right (typeMatch (fst ex1Type) (fst ex2Type), smallestBound (snd ex1Type) (snd ex2Type))
-    where   condType = checkExpression symbolMap cond
+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
+                        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
+                
 
+-- |TODO Handle nested lists and lists with parens
 -- |Checks that all the expressions in a list have compatible types
-checkList :: [Symbol] -> [Expression] -> Either TypeCheckError (Type, Cardinality)
-checkList _ [] = Right (BasicType "Empty", Bounds(0, 0))
-checkList symbs (ex : exps)
-    | isRight typ = checkList1 symbs exps (fromRightUnsafe typ) 
-    | otherwise = typ
-    where typ = checkExpression symbs ex
+checkList :: [Symbol] -> [Expression] -> Either TypeCheckError ExplicitExpression
+checkList _ [] = Right $ ExplicitList [ExplicitEmpty]
+checkList symbs (ex : exps) =
+    case checkExpression symbs ex of
+        Left err -> Left err
+        Right x -> 
+            case checkList1 symbs exps (coercionType $ typeCoercion $ returnCoercion x, toCardinality $ cardinalityCoercion $ returnCoercion x) of
+                Left err -> Left err
+                Right exp -> Right $ ExplicitList exp
     
 -- |Auxiliary function for the check list function
-checkList1 :: [Symbol] -> [Expression] -> (Type, Cardinality) -> Either TypeCheckError (Type, Cardinality)
-checkList1 _ [] typ = Right typ
-checkList1 symbs (ex : exps) typ 
-    | isLeft exTyp = exTyp
-    | sub = checkList1 symbs exps (fst typ, smallestBound (snd $ fromRightUnsafe exTyp) (snd typ))
-    | sup = checkList1 symbs exps (fst $ fromRightUnsafe exTyp, smallestBound (snd $ fromRightUnsafe exTyp) (snd typ))
-    | otherwise = Left $ TypeMismatch (typeName $ fst typ) (typeName $ fst (fromRightUnsafe exTyp))
-    where 
-        exTyp = checkExpression symbs ex 
-        sub = isSubType (fst typ) (fst (fromRightUnsafe exTyp))
-        sup = isSubType (fst (fromRightUnsafe  exTyp)) (fst typ)
+checkList1 :: [Symbol] -> [Expression] -> (Type, Cardinality) -> Either TypeCheckError [ExplicitExpression]
+checkList1 _ [] typ = Right [ExplicitEmpty]
+checkList1 symbs (ex : exps) typ =
+    case checkExpression symbs ex of
+        Left err -> Left err
+        Right exCo -> 
+            case fst typ `isSubType` exTyp of
+                Left err -> Left err
+                Right _ -> 
+                    case checkList1 symbs exps (exTyp, smallestBound exCard (snd typ)) of
+                        Left err -> Left err
+                        Right explicitEx -> Right [ExplicitList explicitEx] 
+                where
+                    exTyp = coercionType $ typeCoercion $ returnCoercion exCo
+                    exCard = toCardinality $ cardinalityCoercion $ returnCoercion exCo
 
 -- |Checks whether the function that is called is already defined with the same argument types
-checkFunctionCall :: [Symbol] -> String -> [Either TypeCheckError (Type, Cardinality)] -> Either TypeCheckError (Type, Cardinality)
+checkFunctionCall :: [Symbol] -> String -> [Either TypeCheckError ExplicitExpression ] -> Either TypeCheckError ExplicitExpression  
 checkFunctionCall [] fun args = Left $ UndefinedFunction $ "Undefined function: \"" ++ fun ++ "\" [" ++ show (rights args) ++ "]"
 checkFunctionCall ((Func n a r):symbolMap) name args
-    | length right /= length args = Left $ ErrorInsideFunction (name ++ ": " ++ show args ++ show (lefts args))
-    | name == n && all isRight (zipWith typeIncluded right a) = Right r
+    | 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))) 
     | otherwise = checkFunctionCall symbolMap name args
     where 
-        right = rights args
+        argCoerce = map returnCoercion (rights args)
+        coerce = zipWith coercionIncluded argCoerce (map createCoercion a)
 checkFunctionCall (_:symbolMap) name args = checkFunctionCall symbolMap name args 
 
-typeIncluded :: (Type, Cardinality) -> (Type, Cardinality) -> Either TypeCheckError Bool
-typeIncluded (t1, c1) (t2, c2)
-    | t1 `isSubType` t2 && cardinalityIncluded c1 c2 = Right True
-    | t1 `isSubType` t2 = Left $ CardinalityMismatch c1 c2
-    | otherwise = Left $ TypeMismatch (typeName t1) (typeName t2)
+typeIncluded :: (Type, Cardinality) -> (Type, Cardinality) -> Either TypeCheckError Coercion
+typeIncluded (t1, c1) (t2, c2) =
+    case t1 `isSubType` t2 of
+        Left err -> Left err
+        Right typeCoercion ->
+            case c1 `cardinalityIncluded` c2 of
+                Left err -> Left err
+                Right cardCoercion -> Right $ MakeCoercion typeCoercion cardCoercion
+
+coercionIncluded :: Coercion -> Coercion -> Either TypeCheckError Coercion 
+coercionIncluded c1 c2 = (coercionType (typeCoercion c1), coercionCardinality [cardinalityCoercion c1]) `typeIncluded` (coercionType (typeCoercion c2), coercionCardinality [cardinalityCoercion c2])  
 
 -- |Finds the most specific super type of the two types
 typeMatch :: Type -> Type -> Type
@@ -163,18 +195,51 @@ typeMatch x (BasicType "Any") = x
 -- |Integer can be a double
 -- typeMatch (BasicType "Integer") (BasicType "Double") = BasicType "Double"
 -- typeMatch (BasicType "Double") (BasicType "Integer") = BasicType "Double"
-typeMatch x (BasicType y) 
-    | x `isSubType` BasicType y = x
-    | otherwise = BasicType "Object"
+typeMatch x (BasicType y) =
+    case x `isSubType` BasicType y of
+        Left err -> BasicType "Object"
+        Right _ -> BasicType y
 -- |First check x with all the supertypes of y, then go higher on the supertypes of x and repeat
-typeMatch x y
-    | x `isSubType` y = x
-    | otherwise = typeMatch x (superType y)
+typeMatch x y = case x `isSubType` y of
+        Left err -> typeMatch x (superType y)
+        Right _ -> y
 
 -- |Looks in the symbol map for the type of a variable
-findVarType :: String -> [Symbol] -> Either TypeCheckError (Type, Cardinality)
+findVarType :: String -> [Symbol] -> Either TypeCheckError ExplicitExpression  
 findVarType var [] = Left $ UndefinedVariable var
 findVarType x ((Var name typ crd):symbols)
-    | x == name = Right (typ, crd)
+    | x == name = Right $ ExplicitVariable x (MakeCoercion [MakeIdCoercion typ] (MakeCardinalityIdCoercion crd))
     | otherwise = findVarType x symbols
-findVarType x (_:symbols) = findVarType x symbols
\ No newline at end of file
+findVarType x (_:symbols) = findVarType x symbols
+
+-- |Checks whether the first argument is a subtype of the second argument
+isSubType :: Type -> Type -> Either TypeCheckError [TypeCoercion]
+isSubType (BasicType "Integer") (BasicType "Double") = Right [MakeTypeCoercion (BasicType "Integer") (BasicType "Double") "fromInteger"]
+isSubType (BasicType x) y 
+    | x == typeName y = Right [MakeTypeCoercion y y "id"]
+    | otherwise = Left $ TypeMismatch x (typeName y) 
+isSubType x y 
+    | typeName x == typeName y = Right [MakeTypeCoercion x y "id"]
+    | otherwise = case isSubType (superType x) y of
+        Left e -> Left e
+        Right transforms -> Right $ MakeTypeCoercion x y "super" : transforms
+
+-- |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) "[]"
+-- |General
+cardinalityIncluded (OneBound x) (OneBound y)
+    | x >= y = Right $ MakeCardinalityCoercion (OneBound x) (OneBound y) "id"
+    | otherwise = Left $ CardinalityMismatch (OneBound x) (OneBound y)
+cardinalityIncluded (Bounds (x1, y1)) (OneBound y)
+    | x1 >= y = Right $ MakeCardinalityCoercion (Bounds (x1, y1)) (OneBound y) "id"
+    | 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"
+    | otherwise = Left $ CardinalityMismatch (Bounds (x1, x2)) (Bounds (y1, y2))
diff --git a/src/Semantic/FunctionChecker.hs b/src/Semantic/FunctionChecker.hs
index e1e02e3..5f90c60 100644
--- a/src/Semantic/FunctionChecker.hs
+++ b/src/Semantic/FunctionChecker.hs
@@ -9,15 +9,17 @@ import Data.Char
 import Utils.Utils
 
 -- |Checks if all the inputs and the output of a function call have valid types, and then checks that the assign-output expression is valid
-checkFunction :: ([Type], [Symbol]) ->  Function -> Either [TypeCheckError] Function
-checkFunction (definedTypes, symbols) (MakeFunction name desc inp out ex)
-    | isRight checkedEx && isRight checkedOut && null (lefts checkedIn) = 
-        case typeIncluded (fromRightUnsafe checkedEx) (attributeType $ fromRightUnsafe checkedOut, Model.Type.cardinality out) of
-            Right _ -> Right $ MakeFunction (toLower (head name) : tail name) desc (rights checkedIn) (fromRightUnsafe checkedOut) ex
-            Left err -> Left [err] 
-    | otherwise = Left $ lefts [checkedOut] ++ lefts checkedIn ++ lefts [checkedEx]
-        where 
-            checkedIn = checkAttributes definedTypes inp
-            localEnv = addVariables symbols inp
-            checkedEx = checkExpression localEnv ex
-            checkedOut = head $ checkAttributes definedTypes [out]
\ No newline at end of file
+checkFunction :: ([Type], [Symbol]) ->  Function -> Either [TypeCheckError] ExplicitFunction
+checkFunction (definedTypes, symbols) (MakeFunction (MakeFunctionSignature name desc inp out) ex) =
+    if null $ lefts checkedIn
+        then
+            case head $ checkAttributes definedTypes [out] of
+                Left err -> Left [err]
+                Right checkedOut -> case checkExpression (addVariables symbols inp) ex of
+                    Left err -> Left [err]
+                    Right checkedEx -> case returnCoercion checkedEx `coercionIncluded` createCoercion (attributeType checkedOut, Model.Type.cardinality out) of
+                        Left err -> Left [err]
+                        Right _ -> Right $ MakeExplicitFunction (MakeFunctionSignature (toLower (head name) : tail name) desc (rights checkedIn) checkedOut) checkedEx
+        else
+            Left $ lefts checkedIn
+    where checkedIn = checkAttributes definedTypes inp
\ No newline at end of file
diff --git a/src/Semantic/TypeChecker.hs b/src/Semantic/TypeChecker.hs
index 63474d0..f896f04 100644
--- a/src/Semantic/TypeChecker.hs
+++ b/src/Semantic/TypeChecker.hs
@@ -41,10 +41,10 @@ populateSuper allTypes (currType : types) (MakeType t super d a c)
 -- |Checks whether all the types of the attributes of a data type are already defined
 checkAttributes :: [Type] -> [TypeAttribute] -> [Either TypeCheckError TypeAttribute]
 checkAttributes _ [] = []
-checkAttributes definedTypes ((MakeTypeAttribute name typ crd desc):as)
-    | isRight checked = Right (MakeTypeAttribute name (fromRightUnsafe checked) crd desc) : checkAttributes definedTypes as
-    | otherwise = Left (fromLeftUnsafe checked) : checkAttributes definedTypes as
-    where checked = checkAttributeType definedTypes typ 
+checkAttributes definedTypes ((MakeTypeAttribute name typ crd desc):as) =
+    case checkAttributeType definedTypes typ of
+        Left err -> Left err : checkAttributes definedTypes as
+        Right checked -> Right (MakeTypeAttribute name checked crd desc) : checkAttributes definedTypes as 
 
 -- |Checks whether a type is predefined or in the symbol table
 checkAttributeType :: [Type] -> Type -> Either TypeCheckError Type
diff --git a/src/Utils/Utils.hs b/src/Utils/Utils.hs
index b1d5180..690bf54 100644
--- a/src/Utils/Utils.hs
+++ b/src/Utils/Utils.hs
@@ -84,18 +84,4 @@ checkDuplicates :: Eq a => [a] -> [a]
 checkDuplicates [] = []
 checkDuplicates (a : as)
     | a `elem` as = a : checkDuplicates as
-    | otherwise = checkDuplicates as
-
--- |Auxiliary function to get the right value from an either that stops with an error if the value is left
--- used when it is certain that the value will be right
-fromRightUnsafe :: Either a b -> b
-fromRightUnsafe x = case x of
-    Left a -> error "Value is Left"
-    Right b -> b
-    
--- |Auxiliary function to get the left value from an either that stops with an error if the value is right
--- used when it is certain that the value will be left
-fromLeftUnsafe :: Either a b -> a
-fromLeftUnsafe x = case x of
-    Left a -> a
-    Right _ -> error "Value is Right"
\ No newline at end of file
+    | otherwise = checkDuplicates as
\ No newline at end of file