Language/Symantic/Typing/Constraint.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE ConstraintKinds #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}
  13 module Language.Symantic.Typing.Constraint where
  14
  15 import Data.Maybe (fromMaybe)
  16 import Data.Proxy
  17 import Data.Type.Equality
  18
  19 import Language.Symantic.Typing.Kind
  20 import Language.Symantic.Typing.Constant
  21 import Language.Symantic.Typing.Type
  22
  23 -- * Type 'Con'
  24 -- | Captures the proof of a 'Constraint'
  25 -- (and its dictionary for a type class):
  26 -- pattern matching on the 'Con' constructor
  27 -- brings the 'Constraint' into scope.
  28 data Con c where
  29         Con :: c => Con c
  30
  31 -- * Type family 'Consts_imported_by'
  32 -- | Return the /type constant/s that a given /type constant/
  33 -- wants to be part of the final list of /type constants/.
  34 type family Consts_imported_by (c::k) :: [*]
  35 type instance Consts_imported_by [] =
  36  [ Proxy Applicative
  37  , Proxy Eq
  38  , Proxy Foldable
  39  , Proxy Functor
  40  , Proxy Monad
  41  , Proxy Monoid
  42  , Proxy Ord
  43  , Proxy Traversable
  44  ]
  45 type instance Consts_imported_by (->) =
  46  [ Proxy Applicative
  47  , Proxy Functor
  48  , Proxy Monad
  49  , Proxy Monoid
  50  ]
  51 type instance Consts_imported_by Applicative = '[]
  52 type instance Consts_imported_by Bool =
  53  [ Proxy Bounded
  54  , Proxy Enum
  55  , Proxy Eq
  56  , Proxy Ord
  57  ]
  58 type instance Consts_imported_by Bounded = '[]
  59 type instance Consts_imported_by Eq = '[]
  60 type instance Consts_imported_by Enum = '[]
  61 type instance Consts_imported_by Foldable = '[]
  62 type instance Consts_imported_by Functor = '[]
  63 type instance Consts_imported_by Int =
  64  [ Proxy Bounded
  65  , Proxy Enum
  66  , Proxy Eq
  67  , Proxy Integral
  68  , Proxy Num
  69  , Proxy Ord
  70  , Proxy Real
  71  ]
  72 type instance Consts_imported_by Integer =
  73  [ Proxy Enum
  74  , Proxy Eq
  75  , Proxy Integral
  76  , Proxy Num
  77  , Proxy Ord
  78  , Proxy Real
  79  ]
  80 type instance Consts_imported_by Integral =
  81  [ Proxy Enum
  82  , Proxy Real
  83  ]
  84 type instance Consts_imported_by IO =
  85  [ Proxy Applicative
  86  , Proxy Functor
  87  , Proxy Monad
  88  ]
  89 type instance Consts_imported_by Maybe =
  90  [ Proxy Applicative
  91  , Proxy Eq
  92  , Proxy Foldable
  93  , Proxy Functor
  94  , Proxy Monad
  95  , Proxy Monoid
  96  , Proxy Traversable
  97  ]
  98 type instance Consts_imported_by Monad = '[]
  99 type instance Consts_imported_by Monoid = '[]
 100 type instance Consts_imported_by Num = '[]
 101 type instance Consts_imported_by Ord = '[]
 102 type instance Consts_imported_by Real = '[]
 103 type instance Consts_imported_by Traversable = '[]
 104
 105 -- * Type 'Proj_Con'
 106 -- | Convenient type synonym wrapping 'Proj_ConR'
 107 -- to initiate its recursion.
 108 type Proj_Con cs = Proj_ConR cs cs
 109
 110 -- | Project the 'Constraint' indexed by the given 'Type'
 111 -- onto its proof, captured by 'Con' when it holds.
 112 proj_con
 113  :: forall cs q. Proj_Con cs
 114  => Type cs 'KiCon q
 115  -> Maybe (Con (UnProxy q))
 116 proj_con = proj_conR (Proxy::Proxy cs)
 117
 118 -- ** Class 'Proj_ConR'
 119 -- | Intermediate type class to construct an instance of 'Proj_Con'
 120 -- from many instances of 'Proj_ConC', one for each item of @cs@.
 121 --
 122 -- * @cs@: starting  list of /type constants/.
 123 -- * @rs@: remaining list of /type constants/.
 124 class Proj_ConR cs rs where
 125         proj_conR :: Proxy rs -> Type cs 'KiCon q -> Maybe (Con (UnProxy q))
 126         proj_conR _rs _q = Nothing
 127
 128 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
 129 -- or recurse on @rs@, preserving the starting list of /type constants/.
 130 instance
 131  ( Proj_ConC cs c
 132  , Proj_ConR cs rs
 133  ) => Proj_ConR cs (c ': rs) where
 134         proj_conR _rs q =
 135                 proj_conR (Proxy::Proxy rs) q `fromMaybe`
 136                 proj_conC (Proxy::Proxy c)  q
 137 -- | End the recursion.
 138 instance Proj_ConR cs '[]
 139
 140 -- ** Class 'Proj_ConC'
 141 -- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
 142 -- that is: maybe it handles the given 'Constraint',
 143 -- and if so, maybe the 'Constraint' holds.
 144 class Proj_ConC cs c where
 145         proj_conC :: Proxy c -> Type cs 'KiCon q -> Maybe (Maybe (Con (UnProxy q)))
 146         proj_conC _c _q = Nothing
 147
 148 instance -- []
 149  ( Proj_Const cs (Proxy [])
 150  , Proj_Consts cs (Consts_imported_by [])
 151  , Proj_Con cs
 152  ) => Proj_ConC cs (Proxy []) where
 153         proj_conC _ (TyConst q :$ TyConst c)
 154          | Just Refl <- proj_const c (Proxy::Proxy [])
 155          = Just $ case () of
 156                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 157                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 158                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 159                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 160                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 161                  _ -> Nothing
 162         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 163          | Just Refl <- proj_const c (Proxy::Proxy [])
 164          = Just $ case () of
 165                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 166                    , Just Con <- proj_con (t :$ a) -> Just Con
 167                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 168                    , Just Con <- proj_con (t :$ a) -> Just Con
 169                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 170                    , Just Con <- proj_con (t :$ a) -> Just Con
 171                  _ -> Nothing
 172         proj_conC _c _q = Nothing
 173 instance -- (->)
 174  ( Proj_Const cs (Proxy (->))
 175  , Proj_Consts cs (Consts_imported_by (->))
 176  , Proj_Con cs
 177  ) => Proj_ConC cs (Proxy (->)) where
 178         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 179          | Just Refl <- proj_const c (Proxy::Proxy (->))
 180          = Just $ case () of
 181                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 182                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 183                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 184                  _ -> Nothing
 185         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 186          | Just Refl <- proj_const c (Proxy::Proxy (->))
 187          = Just $ case () of
 188                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 189                    , Just Con <- proj_con (t :$ b) -> Just Con
 190                  _ -> Nothing
 191         proj_conC _c _q = Nothing
 192 instance -- Applicative
 193  ( Proj_Const cs (Proxy Applicative)
 194  , Proj_Consts cs (Consts_imported_by Applicative)
 195  ) => Proj_ConC cs (Proxy Applicative)
 196 instance -- Bool
 197  ( Proj_Const cs (Proxy Bool)
 198  , Proj_Consts cs (Consts_imported_by Bool)
 199  ) => Proj_ConC cs (Proxy Bool) where
 200         proj_conC _ (TyConst q :$ TyConst c)
 201          | Just Refl <- proj_const c (Proxy::Proxy Bool)
 202          = Just $ case () of
 203                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
 204                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
 205                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
 206                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
 207                  _ -> Nothing
 208         proj_conC _c _q = Nothing
 209 instance -- Bounded
 210  ( Proj_Const cs (Proxy Bounded)
 211  , Proj_Consts cs (Consts_imported_by Bounded)
 212  ) => Proj_ConC cs (Proxy Bounded)
 213 instance -- Enum
 214  ( Proj_Const cs (Proxy Enum)
 215  , Proj_Consts cs (Consts_imported_by Enum)
 216  ) => Proj_ConC cs (Proxy Enum)
 217 instance -- Eq
 218  ( Proj_Const cs (Proxy Eq)
 219  , Proj_Consts cs (Consts_imported_by Eq)
 220  ) => Proj_ConC cs (Proxy Eq)
 221 instance -- Foldable
 222  ( Proj_Const cs (Proxy Foldable)
 223  , Proj_Consts cs (Consts_imported_by Foldable)
 224  ) => Proj_ConC cs (Proxy Foldable)
 225 instance -- Functor
 226  ( Proj_Const cs (Proxy Functor)
 227  , Proj_Consts cs (Consts_imported_by Functor)
 228  ) => Proj_ConC cs (Proxy Functor)
 229 instance -- Int
 230  ( Proj_Const cs (Proxy Int)
 231  , Proj_Consts cs (Consts_imported_by Int)
 232  ) => Proj_ConC cs (Proxy Int) where
 233         proj_conC _ (TyConst q :$ TyConst c)
 234          | Just Refl <- proj_const c (Proxy::Proxy Int)
 235          = Just $ case () of
 236                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
 237                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 238                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 239                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
 240                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
 241                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 242                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
 243                  _ -> Nothing
 244         proj_conC _c _q = Nothing
 245 instance -- Integer
 246  ( Proj_Const cs (Proxy Integer)
 247  , Proj_Consts cs (Consts_imported_by Integer)
 248  ) => Proj_ConC cs (Proxy Integer) where
 249         proj_conC _ (TyConst q :$ TyConst c)
 250          | Just Refl <- proj_const c (Proxy::Proxy Integer)
 251          = Just $ case () of
 252                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 253                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 254                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
 255                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
 256                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 257                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
 258                  _ -> Nothing
 259         proj_conC _c _q = Nothing
 260 instance -- Integral
 261  ( Proj_Const cs (Proxy Integral)
 262  , Proj_Consts cs (Consts_imported_by Integral)
 263  ) => Proj_ConC cs (Proxy Integral)
 264 instance -- IO
 265  ( Proj_Const cs (Proxy IO)
 266  , Proj_Consts cs (Consts_imported_by IO)
 267  ) => Proj_ConC cs (Proxy IO) where
 268         proj_conC _ (TyConst q :$ TyConst c)
 269          | Just Refl <- proj_const c (Proxy::Proxy IO)
 270          = Just $ case () of
 271                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 272                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 273                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 274                  _ -> Nothing
 275         proj_conC _c _q = Nothing
 276 instance -- Maybe
 277  ( Proj_Const cs (Proxy Maybe)
 278  , Proj_Consts cs (Consts_imported_by Maybe)
 279  , Proj_Con cs
 280  ) => Proj_ConC cs (Proxy Maybe) where
 281         proj_conC _ (TyConst q :$ TyConst c)
 282          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 283          = Just $ case () of
 284                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 285                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 286                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 287                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 288                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 289                  _ -> Nothing
 290         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 291          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 292          = Just $ case () of
 293                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 294                    , Just Con <- proj_con (t :$ a) -> Just Con
 295                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 296                    , Just Con <- proj_con (t :$ a) -> Just Con
 297                  _ -> Nothing
 298         proj_conC _c _q = Nothing
 299 instance -- Monad
 300  ( Proj_Const cs (Proxy Monad)
 301  , Proj_Consts cs (Consts_imported_by Monad)
 302  ) => Proj_ConC cs (Proxy Monad)
 303 instance -- Monoid
 304  ( Proj_Const cs (Proxy Monoid)
 305  , Proj_Consts cs (Consts_imported_by Monoid)
 306  ) => Proj_ConC cs (Proxy Monoid)
 307 instance -- Num
 308  ( Proj_Const cs (Proxy Num)
 309  , Proj_Consts cs (Consts_imported_by Num)
 310  ) => Proj_ConC cs (Proxy Num)
 311 instance -- Ord
 312  ( Proj_Const cs (Proxy Ord)
 313  , Proj_Consts cs (Consts_imported_by Ord)
 314  ) => Proj_ConC cs (Proxy Ord)
 315 instance -- Real
 316  ( Proj_Const cs (Proxy Real)
 317  , Proj_Consts cs (Consts_imported_by Real)
 318  ) => Proj_ConC cs (Proxy Real)
 319 instance -- Traversable
 320  ( Proj_Const cs (Proxy Traversable)
 321  , Proj_Consts cs (Consts_imported_by Traversable)
 322  ) => Proj_ConC cs (Proxy Traversable)