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 Control.Applicative ((<|>))
  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 Bounded
  37  , Proxy Enum
  38  , Proxy Eq
  39  , Proxy Monoid
  40  , Proxy Ord
  41  ]
  42 type instance Consts_imported_by Bounded = '[]
  43 type instance Consts_imported_by Enum = '[]
  44 type instance Consts_imported_by Real = '[]
  45 type instance Consts_imported_by String = '[]
  46
  47 -- * Type 'Proj_Con'
  48 -- | Convenient type synonym wrapping 'Proj_ConR'
  49 -- to initiate its recursion.
  50 type Proj_Con cs = Proj_ConR cs cs
  51
  52 -- | Project the 'Constraint' indexed by the given 'Type'
  53 -- onto its proof, captured by 'Con' when it holds.
  54 proj_con
  55  :: forall cs q. Proj_Con cs
  56  => Type cs q
  57  -> Maybe (Con q)
  58 proj_con = proj_conR (Proxy::Proxy cs)
  59
  60 -- ** Class 'Proj_ConR'
  61 -- | Intermediate type class to construct an instance of 'Proj_Con'
  62 -- from many instances of 'Proj_ConC', one for each item of @cs@.
  63 --
  64 -- * @cs@: starting  list of /type constants/.
  65 -- * @rs@: remaining list of /type constants/.
  66 class Proj_ConR cs rs where
  67         proj_conR :: Proxy rs -> Type cs q -> Maybe (Con q)
  68         proj_conR _rs _q = Nothing
  69
  70 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
  71 -- or recurse on @rs@, preserving the starting list of /type constants/.
  72 instance
  73  ( Proj_ConC cs c
  74  , Proj_ConR cs rs
  75  ) => Proj_ConR cs (c ': rs) where
  76         proj_conR _rs q =
  77                 proj_conC (Proxy::Proxy c)  q <|>
  78                 proj_conR (Proxy::Proxy rs) q
  79 -- | End the recursion.
  80 instance Proj_ConR cs '[]
  81
  82 -- ** Class 'Proj_ConC'
  83 -- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
  84 -- that is: maybe it handles the given 'Constraint',
  85 -- and if so, maybe the 'Constraint' holds.
  86 class Proj_ConC cs c where
  87         proj_conC :: Proxy c -> Type cs q -> Maybe (Con q)
  88         proj_conC _c _q = Nothing
  89
  90 instance -- ()
  91  ( Proj_Const cs ()
  92  , Proj_Consts cs (Consts_imported_by ())
  93  ) => Proj_ConC cs (Proxy ()) where
  94         proj_conC _ (TyConst q :$ TyConst c)
  95          | Just Refl <- eq_skind (kind_of_const c) SKiType
  96          , Just Refl <- proj_const c (Proxy::Proxy ())
  97          = case () of
  98                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
  99                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 100                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 101                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)   -> Just Con
 102                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 103                  _ -> Nothing
 104         proj_conC _c _q = Nothing
 105 instance -- Bounded
 106  Proj_ConC cs (Proxy Bounded)
 107 instance -- Enum
 108  Proj_ConC cs (Proxy Enum)
 109 instance -- Real
 110  Proj_ConC cs (Proxy Real)
 111 instance -- String
 112  Proj_ConC cs (Proxy String)