diff --git a/nac3core/src/codegen/concrete_type.rs b/nac3core/src/codegen/concrete_type.rs
index 472f78e..7745160 100644
--- a/nac3core/src/codegen/concrete_type.rs
+++ b/nac3core/src/codegen/concrete_type.rs
@@ -60,9 +60,8 @@ pub enum ConcreteTypeEnum {
         ret: ConcreteType,
         vars: HashMap<u32, ConcreteType>,
     },
-    TConstant {
-        value: SymbolValue,
-        ty: ConcreteType,
+    TLiteral {
+        values: Vec<SymbolValue>,
     },
 }
 
@@ -202,9 +201,8 @@ impl ConcreteTypeStore {
                 TypeEnum::TFunc(signature) => {
                     self.from_signature(unifier, primitives, signature, cache)
                 }
-                TypeEnum::TConstant { value, ty, .. } => ConcreteTypeEnum::TConstant {
-                    value: value.clone(),
-                    ty: self.from_unifier_type(unifier, primitives, *ty, cache),
+                TypeEnum::TLiteral { values, .. } => ConcreteTypeEnum::TLiteral {
+                    values: values.clone(),
                 },
                 _ => unreachable!("{:?}", ty_enum.get_type_name()),
             };
@@ -293,9 +291,8 @@ impl ConcreteTypeStore {
                     .map(|(id, cty)| (*id, self.to_unifier_type(unifier, primitives, *cty, cache)))
                     .collect::<HashMap<_, _>>(),
             }),
-            ConcreteTypeEnum::TConstant { value, ty } => TypeEnum::TConstant {
-                value: value.clone(),
-                ty: self.to_unifier_type(unifier, primitives, *ty, cache),
+            ConcreteTypeEnum::TLiteral { values, .. } => TypeEnum::TLiteral {
+                values: values.clone(),
                 loc: None,
             }
         };
diff --git a/nac3core/src/codegen/mod.rs b/nac3core/src/codegen/mod.rs
index 0917d8c..51496e6 100644
--- a/nac3core/src/codegen/mod.rs
+++ b/nac3core/src/codegen/mod.rs
@@ -580,6 +580,7 @@ pub fn gen_func_impl<'ctx, G: CodeGenerator, F: FnOnce(&mut G, &mut CodeGenConte
         let (unifier, primitives) = &top_level_ctx.unifiers.read()[task.unifier_index];
         (Unifier::from_shared_unifier(unifier), *primitives)
     };
+    unifier.put_primitive_store(&primitives);
     unifier.top_level = Some(top_level_ctx.clone());
 
     let mut cache = HashMap::new();
diff --git a/nac3core/src/symbol_resolver.rs b/nac3core/src/symbol_resolver.rs
index 2f08ecc..0932bea 100644
--- a/nac3core/src/symbol_resolver.rs
+++ b/nac3core/src/symbol_resolver.rs
@@ -114,6 +114,41 @@ impl SymbolValue {
         }
     }
 
+    /// Creates a [`SymbolValue`] from a [`Constant`], with its type being inferred from the constant value.
+    ///
+    /// * `constant` - The constant to create the value from.
+    pub fn from_constant_inferred(
+        constant: &Constant,
+        unifier: &mut Unifier
+    ) -> Result<Self, String> {
+        match constant {
+            Constant::None => Ok(SymbolValue::OptionNone),
+            Constant::Bool(b) => Ok(SymbolValue::Bool(*b)),
+            Constant::Str(s) => Ok(SymbolValue::Str(s.to_string())),
+            Constant::Int(i) => {
+                let i = *i;
+                if i >= 0 {
+                    i32::try_from(i).map(SymbolValue::I32)
+                        .or_else(|_| i64::try_from(i).map(SymbolValue::I64))
+                        .map_err(|_| format!("Literal cannot be expressed as any integral type: {i}"))
+                } else {
+                    u32::try_from(i).map(SymbolValue::U32)
+                        .or_else(|_| u64::try_from(i).map(SymbolValue::U64))
+                        .map_err(|_| format!("Literal cannot be expressed as any integral type: {i}"))
+                }
+            }
+            Constant::Tuple(t) => {
+                let elems = t
+                    .iter()
+                    .map(|constant| Self::from_constant_inferred(constant, unifier))
+                    .collect::<Result<Vec<SymbolValue>, _>>()?;
+                Ok(SymbolValue::Tuple(elems))
+            }
+            Constant::Float(f) => Ok(SymbolValue::Double(*f)),
+            _ => Err(format!("Unsupported value type {constant:?}")),
+        }
+    }
+
     /// Returns the [`Type`] representing the data type of this value.
     pub fn get_type(&self, primitives: &PrimitiveStore, unifier: &mut Unifier) -> Type {
         match self {
diff --git a/nac3core/src/toplevel/composer.rs b/nac3core/src/toplevel/composer.rs
index 68cfb72..8e612a6 100644
--- a/nac3core/src/toplevel/composer.rs
+++ b/nac3core/src/toplevel/composer.rs
@@ -563,7 +563,6 @@ impl TopLevelComposer {
                         &primitive_types,
                         b,
                         vec![(*class_def_id, class_type_vars.clone())].into_iter().collect(),
-                        None,
                     )?;
 
                     if let TypeAnnotation::CustomClass { .. } = &base_ty {
@@ -904,7 +903,6 @@ impl TopLevelComposer {
                             // NOTE: since only class need this, for function
                             // it should be fine to be empty map
                             HashMap::new(),
-                            None,
                         )?;
 
                         let type_vars_within =
@@ -971,7 +969,6 @@ impl TopLevelComposer {
                             // NOTE: since only class need this, for function
                             // it should be fine to be empty map
                             HashMap::new(),
-                            None,
                         )?
                     };
 
@@ -1158,7 +1155,6 @@ impl TopLevelComposer {
                                         vec![(class_id, class_type_vars_def.clone())]
                                             .into_iter()
                                             .collect(),
-                                        None,
                                     )?
                                 };
                                 // find type vars within this method parameter type annotation
@@ -1224,7 +1220,6 @@ impl TopLevelComposer {
                                 primitives,
                                 result,
                                 vec![(class_id, class_type_vars_def.clone())].into_iter().collect(),
-                                None,
                             )?;
                             // find type vars within this return type annotation
                             let type_vars_within =
@@ -1319,7 +1314,6 @@ impl TopLevelComposer {
                                 primitives,
                                 annotation.as_ref(),
                                 vec![(class_id, class_type_vars_def.clone())].into_iter().collect(),
-                                None,
                             )?;
                             // find type vars within this return type annotation
                             let type_vars_within =
diff --git a/nac3core/src/toplevel/helper.rs b/nac3core/src/toplevel/helper.rs
index e11de99..0f4d375 100644
--- a/nac3core/src/toplevel/helper.rs
+++ b/nac3core/src/toplevel/helper.rs
@@ -145,6 +145,7 @@ impl TopLevelComposer {
             exception,
             option,
         };
+        unifier.put_primitive_store(&primitives);
         crate::typecheck::magic_methods::set_primitives_magic_methods(&primitives, &mut unifier);
         (primitives, unifier)
     }
diff --git a/nac3core/src/toplevel/type_annotation.rs b/nac3core/src/toplevel/type_annotation.rs
index a44de76..3cd2f25 100644
--- a/nac3core/src/toplevel/type_annotation.rs
+++ b/nac3core/src/toplevel/type_annotation.rs
@@ -1,5 +1,6 @@
 use crate::symbol_resolver::SymbolValue;
 use super::*;
+use nac3parser::ast::Constant;
 
 #[derive(Clone, Debug)]
 pub enum TypeAnnotation {
@@ -13,16 +14,8 @@ pub enum TypeAnnotation {
     // can only be CustomClassKind
     Virtual(Box<TypeAnnotation>),
     TypeVar(Type),
-    /// A constant used in the context of a const-generic variable.
-    Constant {
-        /// The non-type variable associated with this constant.
-        ///
-        /// Invoking [Unifier::get_ty] on this type will return a [TypeEnum::TVar] representing the
-        /// const generic variable of which this constant is associated with.
-        ty: Type,
-        /// The constant value of this constant.
-        value: SymbolValue
-    },
+    /// A `Literal` allowing a subset of literals.
+    Literal(Vec<Constant>),
     List(Box<TypeAnnotation>),
     Tuple(Vec<TypeAnnotation>),
 }
@@ -57,7 +50,7 @@ impl TypeAnnotation {
                     }
                 )
             }
-            Constant { value, .. } => format!("Const({value})"),
+            Literal(values) => format!("Literal({})", values.iter().map(|v| format!("{v:?}")).join(", ")),
             Virtual(ty) => format!("virtual[{}]", ty.stringify(unifier)),
             List(ty) => format!("list[{}]", ty.stringify(unifier)),
             Tuple(types) => {
@@ -81,7 +74,6 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
     expr: &ast::Expr<T>,
     // the key stores the type_var of this topleveldef::class, we only need this field here
     locked: HashMap<DefinitionId, Vec<Type>>,
-    type_var: Option<Type>,
 ) -> Result<TypeAnnotation, HashSet<String>> {
     let name_handle = |id: &StrRef,
                        unifier: &mut Unifier,
@@ -191,8 +183,7 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                 }
                 let result = params_ast
                     .iter()
-                    .enumerate()
-                    .map(|(idx, x)| {
+                    .map(|x| {
                         parse_ast_to_type_annotation_kinds(
                             resolver,
                             top_level_defs,
@@ -203,7 +194,6 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                                 locked.insert(obj_id, type_vars.clone());
                                 locked.clone()
                             },
-                            Some(type_vars[idx]),
                         )
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -239,7 +229,6 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                 primitives,
                 slice.as_ref(),
                 locked,
-                None,
             )?;
             if !matches!(def, TypeAnnotation::CustomClass { .. }) {
                 unreachable!("must be concretized custom class kind in the virtual")
@@ -260,7 +249,6 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                 primitives,
                 slice.as_ref(),
                 locked,
-                None,
             )?;
             Ok(TypeAnnotation::List(def_ann.into()))
         }
@@ -278,7 +266,6 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                 primitives,
                 slice.as_ref(),
                 locked,
-                None,
             )?;
             let id =
                 if let TypeEnum::TObj { obj_id, .. } = unifier.get_ty(primitives.option).as_ref() {
@@ -312,13 +299,51 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
                         primitives,
                         e,
                         locked.clone(),
-                        None,
                     )
                 })
                 .collect::<Result<Vec<_>, _>>()?;
             Ok(TypeAnnotation::Tuple(type_annotations))
         }
 
+        // Literal
+        ast::ExprKind::Subscript { value, slice, .. }
+        if {
+            matches!(&value.node, ast::ExprKind::Name { id, .. } if id == &"Literal".into())
+        } => {
+            let tup_elts = {
+                if let ast::ExprKind::Tuple { elts, .. } = &slice.node {
+                    elts.as_slice()
+                } else {
+                    std::slice::from_ref(slice.as_ref())
+                }
+            };
+            let type_annotations = tup_elts
+                .iter()
+                .map(|e| {
+                    match &e.node {
+                        ast::ExprKind::Constant { value, .. } => Ok(
+                            TypeAnnotation::Literal(vec![value.clone()]),
+                        ),
+                        _ => parse_ast_to_type_annotation_kinds(
+                            resolver,
+                            top_level_defs,
+                            unifier,
+                            primitives,
+                            e,
+                            locked.clone(),
+                        ),
+                    }
+                })
+                .collect::<Result<Vec<_>, _>>()?
+                .into_iter()
+                .flat_map(|type_ann| match type_ann {
+                    TypeAnnotation::Literal(values) => values,
+                    _ => unreachable!(),
+                })
+                .collect_vec();
+            Ok(TypeAnnotation::Literal(type_annotations))
+        }
+
         // custom class
         ast::ExprKind::Subscript { value, slice, .. } => {
             if let ast::ExprKind::Name { id, .. } = &value.node {
@@ -331,30 +356,7 @@ pub fn parse_ast_to_type_annotation_kinds<T>(
         }
 
         ast::ExprKind::Constant { value, .. } => {
-            let type_var = type_var.expect("Expect type variable to be present");
-
-            let ntv_ty_enum = unifier.get_ty_immutable(type_var);
-            let TypeEnum::TVar { range: underlying_ty, .. } = ntv_ty_enum.as_ref() else {
-                unreachable!()
-            };
-            let underlying_ty = underlying_ty[0];
-
-            let value = SymbolValue::from_constant(value, underlying_ty, primitives, unifier)
-                .map_err(|err| HashSet::from([err]))?;
-
-            if matches!(value, SymbolValue::Str(_) | SymbolValue::Tuple(_) | SymbolValue::OptionSome(_)) {
-                return Err(HashSet::from([
-                    format!(
-                        "expression {value} is not allowed for constant type annotation (at {})",
-                        expr.location
-                    ),
-                ]))
-            }
-
-            Ok(TypeAnnotation::Constant {
-                ty: type_var,
-                value,
-            })
+            Ok(TypeAnnotation::Literal(vec![value.clone()]))
         }
 
         _ => Err(HashSet::from([
@@ -390,17 +392,17 @@ pub fn get_type_from_type_annotation_kinds(
                 ]))
             }
 
-                    let param_ty = params
-                        .iter()
-                        .map(|x| {
-                            get_type_from_type_annotation_kinds(
-                                top_level_defs,
-                                unifier,
-                                x,
-                                subst_list
-                            )
-                        })
-                        .collect::<Result<Vec<_>, _>>()?;
+            let param_ty = params
+                .iter()
+                .map(|x| {
+                    get_type_from_type_annotation_kinds(
+                        top_level_defs,
+                        unifier,
+                        x,
+                        subst_list
+                    )
+                })
+                .collect::<Result<Vec<_>, _>>()?;
 
             let subst = {
                 // check for compatible range
@@ -495,14 +497,13 @@ pub fn get_type_from_type_annotation_kinds(
             Ok(ty)
         }
         TypeAnnotation::Primitive(ty) | TypeAnnotation::TypeVar(ty) => Ok(*ty),
-        TypeAnnotation::Constant { ty, value, .. } => {
-            let ty_enum = unifier.get_ty(*ty);
-            let TypeEnum::TVar { range: ntv_underlying_ty, loc, is_const_generic: true, .. } = &*ty_enum else {
-                unreachable!("{} ({})", unifier.stringify(*ty), ty_enum.get_type_name());
-            };
+        TypeAnnotation::Literal(values) => {
+            let values = values.iter()
+                .map(|v| SymbolValue::from_constant_inferred(v, unifier))
+                .collect::<Result<Vec<_>, _>>()
+                .map_err(|err| HashSet::from([err]))?;
 
-            let ty = ntv_underlying_ty[0];
-            let var = unifier.get_fresh_constant(value.clone(), ty, *loc);
+            let var = unifier.get_fresh_literal(values, None);
             Ok(var)
         }
         TypeAnnotation::Virtual(ty) => {
@@ -576,7 +577,7 @@ pub fn get_type_var_contained_in_type_annotation(ann: &TypeAnnotation) -> Vec<Ty
                 result.extend(get_type_var_contained_in_type_annotation(a));
             }
         }
-        TypeAnnotation::Primitive(..) | TypeAnnotation::Constant { .. } => {}
+        TypeAnnotation::Primitive(..) | TypeAnnotation::Literal { .. } => {}
     }
     result
 }
diff --git a/nac3core/src/typecheck/type_inferencer/test.rs b/nac3core/src/typecheck/type_inferencer/test.rs
index 4589c83..f3ac2d0 100644
--- a/nac3core/src/typecheck/type_inferencer/test.rs
+++ b/nac3core/src/typecheck/type_inferencer/test.rs
@@ -148,6 +148,7 @@ impl TestEnvironment {
             uint64,
             option,
         };
+        unifier.put_primitive_store(&primitives);
         set_primitives_magic_methods(&primitives, &mut unifier);
 
         let id_to_name = [
@@ -296,6 +297,8 @@ impl TestEnvironment {
             option,
         };
 
+        unifier.put_primitive_store(&primitives);
+
         let (v0, id) = unifier.get_dummy_var();
 
         let foo_ty = unifier.add_ty(TypeEnum::TObj {
diff --git a/nac3core/src/typecheck/typedef/mod.rs b/nac3core/src/typecheck/typedef/mod.rs
index 85dfedc..4a45c6f 100644
--- a/nac3core/src/typecheck/typedef/mod.rs
+++ b/nac3core/src/typecheck/typedef/mod.rs
@@ -13,6 +13,7 @@ use super::type_error::{TypeError, TypeErrorKind};
 use super::unification_table::{UnificationKey, UnificationTable};
 use crate::symbol_resolver::SymbolValue;
 use crate::toplevel::{DefinitionId, TopLevelContext, TopLevelDef};
+use crate::typecheck::type_inferencer::PrimitiveStore;
 
 #[cfg(test)]
 mod test;
@@ -139,12 +140,10 @@ pub enum TypeEnum {
         is_const_generic: bool,
     },
 
-    /// A constant for substitution into a const generic variable.
-    TConstant {
+    /// A literal generic type matching `typing.Literal`.
+    TLiteral {
         /// The value of the constant.
-        value: SymbolValue,
-        /// The underlying type of the value.
-        ty: Type,
+        values: Vec<SymbolValue>,
         loc: Option<Location>,
     },
 
@@ -191,7 +190,7 @@ impl TypeEnum {
         match self {
             TypeEnum::TRigidVar { .. } => "TRigidVar",
             TypeEnum::TVar { .. } => "TVar",
-            TypeEnum::TConstant { .. } => "TConstant",
+            TypeEnum::TLiteral { .. } => "TConstant",
             TypeEnum::TTuple { .. } => "TTuple",
             TypeEnum::TList { .. } => "TList",
             TypeEnum::TObj { .. } => "TObj",
@@ -211,7 +210,8 @@ pub struct Unifier {
     pub(crate) calls: Vec<Rc<Call>>,
     var_id: u32,
     unify_cache: HashSet<(Type, Type)>,
-    snapshot: Option<(usize, u32)>
+    snapshot: Option<(usize, u32)>,
+    primitive_store: Option<PrimitiveStore>,
 }
 
 impl Default for Unifier {
@@ -231,9 +231,19 @@ impl Unifier {
             unify_cache: HashSet::new(),
             top_level: None,
             snapshot: None,
+            primitive_store: None,
         }
     }
 
+    /// Sets the [PrimitiveStore] instance within this `Unifier`.
+    ///
+    /// This function can only be invoked once. Any subsequent invocations will result in an
+    /// assertion error..
+    pub fn put_primitive_store(&mut self, primitives: &PrimitiveStore) {
+        assert!(self.primitive_store.is_none());
+        self.primitive_store.replace(primitives.clone());
+    }
+
     pub unsafe fn get_unification_table(&mut self) -> &mut UnificationTable<Rc<TypeEnum>> {
         &mut self.unification_table
     }
@@ -252,6 +262,7 @@ impl Unifier {
             top_level: None,
             unify_cache: HashSet::new(),
             snapshot: None,
+            primitive_store: None,
         }
     }
 
@@ -358,8 +369,7 @@ impl Unifier {
         (self.add_ty(TypeEnum::TVar { id, range, fields: None, name, loc, is_const_generic: false }), id)
     }
 
-    /// Returns a fresh type representing a constant generic variable with the given underlying type
-    /// `ty`.
+    /// Returns a fresh type representing a constant generic variable with the given underlying type `ty`.
     pub fn get_fresh_const_generic_var(
         &mut self,
         ty: Type,
@@ -371,17 +381,17 @@ impl Unifier {
         (self.add_ty(TypeEnum::TVar { id, range: vec![ty], fields: None, name, loc, is_const_generic: true }), id)
     }
 
-    /// Returns a fresh type representing a [fresh constant][TypeEnum::TConstant] with the given
-    /// `value` and type `ty`.
-    pub fn get_fresh_constant(
+    /// Returns a fresh type representing a [literal][TypeEnum::TConstant] with the given `values`.
+    pub fn get_fresh_literal(
         &mut self,
-        value: SymbolValue,
-        ty: Type,
+        values: Vec<SymbolValue>,
         loc: Option<Location>,
     ) -> Type {
-        assert!(matches!(self.get_ty(ty).as_ref(), TypeEnum::TObj { .. }));
-
-        self.add_ty(TypeEnum::TConstant { ty, value, loc })
+        let ty_enum = TypeEnum::TLiteral {
+            values: values.into_iter().dedup().collect(),
+            loc
+        };
+        self.add_ty(ty_enum)
     }
 
     /// Unification would not unify rigid variables with other types, but we want to do this for
@@ -456,7 +466,7 @@ impl Unifier {
     pub fn is_concrete(&mut self, a: Type, allowed_typevars: &[Type]) -> bool {
         use TypeEnum::*;
         match &*self.get_ty(a) {
-            TRigidVar { .. } | TConstant { .. } => true,
+            TRigidVar { .. } | TLiteral { .. } => true,
             TVar { .. } => allowed_typevars.iter().any(|b| self.unification_table.unioned(a, *b)),
             TCall { .. } => false,
             TList { ty } | TVirtual { ty } => self.is_concrete(*ty, allowed_typevars),
@@ -519,10 +529,12 @@ impl Unifier {
             }
             required.pop();
             let (name, expected) = all_names.pop().unwrap();
+            let snapshot = self.unification_table.get_snapshot();
             self.unify_impl(expected, *t, false).map_err(|_| {
                 self.restore_snapshot();
                 TypeError::new(TypeErrorKind::IncorrectArgType { name, expected, got: *t }, *loc)
             })?;
+            self.unification_table.restore_snapshot(snapshot);
         }
         for (k, t) in kwargs {
             if let Some(i) = required.iter().position(|v| v == k) {
@@ -536,10 +548,12 @@ impl Unifier {
                     TypeError::new(TypeErrorKind::UnknownArgName(*k), *loc)
                 })?;
             let (name, expected) = all_names.remove(i);
+            let snapshot = self.unification_table.get_snapshot();
             self.unify_impl(expected, *t, false).map_err(|_| {
                 self.restore_snapshot();
                 TypeError::new(TypeErrorKind::IncorrectArgType { name, expected, got: *t }, *loc)
             })?;
+            self.unification_table.restore_snapshot(snapshot);
         }
         if !required.is_empty() {
             self.restore_snapshot();
@@ -734,18 +748,56 @@ impl Unifier {
                 self.set_a_to_b(a, b);
             }
 
-            (TVar { range: ty1, is_const_generic: true, .. }, TConstant { ty: ty2, .. }) => {
-                let ty1 = ty1[0];
+            (TVar { range: tys, is_const_generic: true, .. }, TLiteral { values, .. }) => {
+                assert_eq!(tys.len(), 1);
 
-                self.unify_impl(ty1, *ty2, false)?;
-                self.set_a_to_b(a, b);
+                let primitives = &self.primitive_store
+                    .expect("Expected PrimitiveStore to be present");
+
+                let ty = tys[0];
+
+                for value in values {
+                    let value_ty = value.get_type(primitives, self);
+
+                    if self.unioned(ty, value_ty) {
+                        self.set_a_to_b(a, b);
+                        return Ok(())
+                    }
+
+                    // The types don't match, try to implicitly promote integers
+                    let num_val = match *value {
+                        SymbolValue::I32(v) => v as i128,
+                        SymbolValue::I64(v) => v as i128,
+                        SymbolValue::U32(v) => v as i128,
+                        SymbolValue::U64(v) => v as i128,
+                        _ => return self.incompatible_types(a, b),
+                    };
+
+                    let can_convert = if self.unioned(ty, primitives.int32) {
+                        i32::try_from(num_val).is_ok()
+                    } else if self.unioned(ty, primitives.int64) {
+                        i64::try_from(num_val).is_ok()
+                    } else if self.unioned(ty, primitives.uint32) {
+                        u32::try_from(num_val).is_ok()
+                    } else if self.unioned(ty, primitives.uint64) {
+                        u64::try_from(num_val).is_ok()
+                    } else {
+                        false
+                    };
+
+                    if can_convert {
+                        self.set_a_to_b(a, b);
+                        return Ok(())
+                    }
+                }
+
+                return self.incompatible_types(a, b)
             }
 
-            (TConstant { value: val1, ty: ty1, .. }, TConstant { value: val2, ty: ty2, .. }) => {
-                if val1 != val2 {
+            (TLiteral { values: val1, .. }, TLiteral { values: val2, .. }) => {
+                if val2.iter().any(|val| !val1.contains(val)) {
                     return self.incompatible_types(a, b)
                 }
-                self.unify_impl(*ty1, *ty2, false)?;
 
                 self.set_a_to_b(a, b);
             }
@@ -1003,8 +1055,8 @@ impl Unifier {
                 };
                 n
             }
-            TypeEnum::TConstant { value, .. } => {
-                format!("const({value})")
+            TypeEnum::TLiteral { values, .. } => {
+                format!("const({})", values.iter().map(|v| format!("{v:?}")).join(", "))
             }
             TypeEnum::TTuple { ty } => {
                 let mut fields =
diff --git a/nac3standalone/demo/src/const_generic.py b/nac3standalone/demo/src/const_generic.py
index 2ddca99..1d917ff 100644
--- a/nac3standalone/demo/src/const_generic.py
+++ b/nac3standalone/demo/src/const_generic.py
@@ -16,32 +16,40 @@ class HybridGenericClass2(Generic[A, T]):
 class HybridGenericClass3(Generic[T, A, B]):
     pass
 
-def make_generic_2() -> ConstGenericClass[2]:
+def make_generic_1() -> ConstGenericClass[Literal[1]]:
     return ...
 
-def make_generic2_1_2() -> ConstGeneric2Class[1, 2]:
+def make_generic_2() -> ConstGenericClass[Literal[2]]:
     return ...
 
-def make_hybrid_class_2_int32() -> HybridGenericClass2[2, int32]:
+def make_generic2_1_2() -> ConstGeneric2Class[Literal[1], Literal[2]]:
     return ...
 
-def make_hybrid_class_i32_0_1() -> HybridGenericClass3[int32, 0, 1]:
+def make_hybrid_class_2_int32() -> HybridGenericClass2[Literal[2], int32]:
     return ...
 
-def consume_generic_2(instance: ConstGenericClass[2]):
+def make_hybrid_class_i32_0_1() -> HybridGenericClass3[int32, Literal[0], Literal[1]]:
+    return ...
+
+def consume_generic_1_or_2(instance: ConstGenericClass[Literal[1, 2]]):
     pass
 
-def consume_generic2_1_2(instance: ConstGeneric2Class[1, 2]):
+def consume_generic_2(instance: ConstGenericClass[Literal[2]]):
     pass
 
-def consume_hybrid_class_2_i32(instance: HybridGenericClass2[2, int32]):
+def consume_generic2_1_2(instance: ConstGeneric2Class[Literal[1], Literal[2]]):
     pass
 
-def consume_hybrid_class_i32_0_1(instance: HybridGenericClass3[int32, 0, 1]):
+def consume_hybrid_class_2_i32(instance: HybridGenericClass2[Literal[2], int32]):
+    pass
+
+def consume_hybrid_class_i32_0_1(instance: HybridGenericClass3[int32, Literal[0], Literal[1]]):
     pass
 
 def f():
     consume_generic_2(make_generic_2())
+    consume_generic_1_or_2(make_generic_1())
+    consume_generic_1_or_2(make_generic_2())
     consume_generic2_1_2(make_generic2_1_2())
     consume_hybrid_class_2_i32(make_hybrid_class_2_int32())
     consume_hybrid_class_i32_0_1(make_hybrid_class_i32_0_1())
diff --git a/nac3standalone/src/basic_symbol_resolver.rs b/nac3standalone/src/basic_symbol_resolver.rs
index cdc3575..e483c6d 100644
--- a/nac3standalone/src/basic_symbol_resolver.rs
+++ b/nac3standalone/src/basic_symbol_resolver.rs
@@ -64,7 +64,9 @@ impl SymbolResolver for Resolver {
 
     fn get_identifier_def(&self, id: StrRef) -> Result<DefinitionId, HashSet<String>> {
         self.0.id_to_def.lock().get(&id).copied()
-            .ok_or_else(|| HashSet::from(["Undefined identifier".to_string()]))
+            .ok_or_else(|| HashSet::from([
+                format!("Undefined identifier `{id}`"),
+            ]))
     }
 
     fn get_string_id(&self, s: &str) -> i32 {
diff --git a/nac3standalone/src/main.rs b/nac3standalone/src/main.rs
index f34f55a..eb746a8 100644
--- a/nac3standalone/src/main.rs
+++ b/nac3standalone/src/main.rs
@@ -104,7 +104,6 @@ fn handle_typevar_definition(
                         primitives,
                         x,
                         HashMap::default(),
-                        None,
                     )?;
                     get_type_from_type_annotation_kinds(
                         def_list, unifier, &ty, &mut None
@@ -146,7 +145,6 @@ fn handle_typevar_definition(
                 primitives,
                 &args[1],
                 HashMap::default(),
-                None,
             )?;
             let constraint = get_type_from_type_annotation_kinds(
                 def_list, unifier, &ty, &mut None