1 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE TypeOperators #-}
8 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
9 module Language.Symantic.Type.Int where
11 import Data.Maybe (isJust)
12 import Data.Type.Equality ((:~:)(Refl))
14 import Language.Symantic.Type.Common
18 data Type_Int (root:: * -> *) h where
19 Type_Int :: Type_Int root Int
20 type instance Root_of_Type (Type_Int root) = root
21 type instance Error_of_Type ast (Type_Int root) = No_Error_Type
24 Eq_Type (Type_Int root) where
25 eq_type Type_Int Type_Int = Just Refl
27 Eq (Type_Int root h) where
28 x == y = isJust $ x `eq_type` y
29 instance -- String_from_Type
30 String_from_Type (Type_Int root) where
31 string_from_type Type_Int = "Int"
33 Show (Type_Int root h) where
34 show = string_from_type
35 instance Constraint_Type Eq (Type_Int root) where
36 constraint_type _c Type_Int = Just Dict
37 instance Constraint_Type Ord (Type_Int root) where
38 constraint_type _c Type_Int = Just Dict
39 instance Unlift_Type1 Type_Int
40 instance Eq_Type1 (Type_Int root)
42 -- | Convenient alias to include a 'Type_Int' within a type.
43 type_int :: Type_Root_Lift Type_Int root => root Int
44 type_int = type_root_lift Type_Int