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=7 #-}
  13 module Language.Symantic.Typing.Constraint where
  14
  15 import Data.Maybe (fromMaybe)
  16 import Data.Proxy
  17 import Data.Type.Equality
  18 import GHC.Exts (Constraint)
  19
  20 import Language.Symantic.Typing.Kind
  21 import Language.Symantic.Typing.Constant
  22 import Language.Symantic.Typing.Type
  23
  24 -- * Type 'Con'
  25 -- | Captures the proof of a 'Constraint'
  26 -- (and its dictionary for a type class):
  27 -- pattern matching on the 'Con' constructor
  28 -- brings the 'Constraint' into scope.
  29 data Con c where
  30         Con :: c => Con c
  31
  32 -- * Type family 'Consts_imported_by'
  33 -- | Return the /type constant/s that a given /type constant/
  34 -- wants to be part of the final list of /type constants/.
  35 type family Consts_imported_by (c::k) :: [*]
  36 type instance Consts_imported_by () =
  37  [ Proxy Bounded
  38  , Proxy Enum
  39  , Proxy Eq
  40  , Proxy Monoid
  41  , Proxy Ord
  42  ]
  43
  44 type instance Consts_imported_by Bounded = '[]
  45 type instance Consts_imported_by Enum = '[]
  46 type instance Consts_imported_by Real = '[]
  47 type instance Consts_imported_by String = '[]
  48
  49 -- * Type 'Proj_Con'
  50 -- | Convenient type synonym wrapping 'Proj_ConR'
  51 -- to initiate its recursion.
  52 type Proj_Con cs = Proj_ConR cs cs
  53
  54 -- | Project the 'Constraint' indexed by the given 'Type'
  55 -- onto its proof, captured by 'Con' when it holds.
  56 proj_con
  57  :: forall cs q. Proj_Con cs
  58  => Type cs (q::Constraint)
  59  -> Maybe (Con q)
  60 proj_con = proj_conR (Proxy::Proxy cs)
  61
  62 -- ** Class 'Proj_ConR'
  63 -- | Intermediate type class to construct an instance of 'Proj_Con'
  64 -- from many instances of 'Proj_ConC', one for each item of @cs@.
  65 --
  66 -- * @cs@: starting  list of /type constants/.
  67 -- * @rs@: remaining list of /type constants/.
  68 class Proj_ConR cs rs where
  69         proj_conR :: Proxy rs -> Type cs (q::Constraint) -> Maybe (Con q)
  70         proj_conR _rs _q = Nothing
  71
  72 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
  73 -- or recurse on @rs@, preserving the starting list of /type constants/.
  74 instance
  75  ( Proj_ConC cs c
  76  , Proj_ConR cs rs
  77  ) => Proj_ConR cs (c ': rs) where
  78         proj_conR _rs q =
  79                 proj_conR (Proxy::Proxy rs) q `fromMaybe`
  80                 proj_conC (Proxy::Proxy c)  q
  81 -- | End the recursion.
  82 instance Proj_ConR cs '[]
  83
  84 -- ** Class 'Proj_ConC'
  85 -- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
  86 -- that is: maybe it handles the given 'Constraint',
  87 -- and if so, maybe the 'Constraint' holds.
  88 class Proj_ConC cs c where
  89         proj_conC :: Proxy c -> Type cs (q::Constraint) -> Maybe (Maybe (Con q))
  90         proj_conC _c _q = Nothing
  91
  92 instance -- Bounded
  93  Proj_ConC cs (Proxy Bounded)
  94 instance -- Enum
  95  Proj_ConC cs (Proxy Enum)
  96 instance -- Real
  97  Proj_ConC cs (Proxy Real)
  98 instance -- ()
  99  ( Proj_Const cs ()
 100  , Proj_Consts cs (Consts_imported_by ())
 101  ) => Proj_ConC cs (Proxy ()) where
 102         proj_conC _ (TyConst q :$ TyConst c)
 103          | Just Refl <- eq_skind (kind_of_const c) SKiType
 104          , Just Refl <- proj_const c (Proxy::Proxy ())
 105          = Just $ case () of
 106                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
 107                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 108                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 109                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)   -> Just Con
 110                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 111                  _ -> Nothing
 112         proj_conC _c _q = Nothing
 113 instance -- String
 114  Proj_ConC cs (Proxy String)