symantic/Language/Symantic/Typing/Constraint.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   6 module Language.Symantic.Typing.Constraint where
   7
   8 import Control.Applicative ((<|>))
   9 import Data.Proxy
  10
  11 import Language.Symantic.Typing.Type
  12
  13 -- * Type 'TyCon'
  14 -- | Captures the proof of a 'Constraint'
  15 -- (and its dictionary for a type class):
  16 -- pattern matching on the 'TyCon' constructor
  17 -- brings the 'Constraint' into scope.
  18 data TyCon c where
  19         TyCon :: c => TyCon c
  20
  21 -- * Type family 'TyConsts_imported_by'
  22 -- | Return the /type constant/s that a given /type constant/
  23 -- wants to be part of the final list of /type constants/.
  24 type family TyConsts_imported_by (c::k) :: [*]
  25 type instance TyConsts_imported_by Bounded = '[]
  26 type instance TyConsts_imported_by Enum    = '[]
  27 type instance TyConsts_imported_by Real    = '[]
  28
  29 -- * Type 'Proj_TyCon'
  30 -- | Convenient type synonym wrapping 'Proj_TyConR'
  31 -- to initiate its recursion.
  32 type Proj_TyCon cs = Proj_TyConR cs cs
  33
  34 -- | Project the 'Constraint' indexed by the given 'Type'
  35 -- onto its proof, captured by 'TyCon' when it holds.
  36 proj_TyCon
  37  :: forall cs q. Proj_TyCon cs
  38  => Type cs q
  39  -> Maybe (TyCon q)
  40 proj_TyCon = proj_TyConR (Proxy @cs)
  41
  42 -- ** Class 'Proj_TyConR'
  43 -- | Intermediate type class to construct an instance of 'Proj_TyCon'
  44 -- from many instances of 'Proj_TyConC', one for each item of @cs@.
  45 --
  46 -- * @cs@: starting  list of /type constants/.
  47 -- * @rs@: remaining list of /type constants/.
  48 class Proj_TyConR cs rs where
  49         proj_TyConR :: Proxy rs -> Type cs q -> Maybe (TyCon q)
  50         proj_TyConR _rs _q = Nothing
  51
  52 -- | Test whether @c@ handles the work of 'Proj_TyCon' or not,
  53 -- or recurse on @rs@, preserving the starting list of /type constants/.
  54 instance
  55  ( Proj_TyConC cs c
  56  , Proj_TyConR cs rs
  57  ) => Proj_TyConR cs (c ': rs) where
  58         proj_TyConR _rs q =
  59                 proj_TyConC (Proxy @c)  q <|>
  60                 proj_TyConR (Proxy @rs) q
  61 -- | End the recursion.
  62 instance Proj_TyConR cs '[]
  63
  64 -- ** Class 'Proj_TyConC'
  65 -- | Handle the work of 'Proj_TyCon' for a given /type constant/ @c@,
  66 -- that is: maybe it handles the given 'Constraint',
  67 -- and if so, maybe the 'Constraint' holds.
  68 class Proj_TyConC cs c where
  69         proj_TyConC :: Proxy c -> Type cs q -> Maybe (TyCon q)
  70         proj_TyConC _c _q = Nothing
  71
  72 instance Proj_TyConC cs (Proxy Bounded)
  73 instance Proj_TyConC cs (Proxy Enum)
  74 instance Proj_TyConC cs (Proxy Real)