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