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
  26 -- * Type 'Proj_TyCon'
  27 -- | Convenient type synonym wrapping 'Proj_TyConR'
  28 -- to initiate its recursion.
  29 type Proj_TyCon cs = Proj_TyConR cs cs
  30
  31 -- | Project the 'Constraint' indexed by the given 'Type'
  32 -- onto its proof, captured by 'TyCon' when it holds.
  33 proj_TyCon
  34  :: forall cs q. Proj_TyCon cs
  35  => Type cs q
  36  -> Maybe (TyCon q)
  37 proj_TyCon = proj_TyConR (Proxy @cs)
  38
  39 -- ** Class 'Proj_TyConR'
  40 -- | Intermediate type class to construct an instance of 'Proj_TyCon'
  41 -- from many instances of 'Proj_TyConC', one for each item of @cs@.
  42 --
  43 -- * @cs@: starting  list of /type constants/.
  44 -- * @rs@: remaining list of /type constants/.
  45 class Proj_TyConR cs rs where
  46         proj_TyConR :: Proxy rs -> Type cs q -> Maybe (TyCon q)
  47         proj_TyConR _rs _q = Nothing
  48
  49 -- | Test whether @c@ handles the work of 'Proj_TyCon' or not,
  50 -- or recurse on @rs@, preserving the starting list of /type constants/.
  51 instance
  52  ( Proj_TyConC cs c
  53  , Proj_TyConR cs rs
  54  ) => Proj_TyConR cs (c ': rs) where
  55         proj_TyConR _rs q =
  56                 proj_TyConC (Proxy @c)  q <|>
  57                 proj_TyConR (Proxy @rs) q
  58 -- | End the recursion.
  59 instance Proj_TyConR cs '[]
  60
  61 -- ** Class 'Proj_TyConC'
  62 -- | Handle the work of 'Proj_TyCon' for a given /type constant/ @c@,
  63 -- that is: maybe it handles the given 'Constraint',
  64 -- and if so, maybe the 'Constraint' holds.
  65 class Proj_TyConC cs c where
  66         proj_TyConC :: Proxy c -> Type cs q -> Maybe (TyCon q)
  67         proj_TyConC _c _q = Nothing