symantic/Language/Symantic/Typing/Constraint.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# LANGUAGE UndecidableSuperClasses #-}
   6 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   7 module Language.Symantic.Typing.Constraint where
   8
   9 import Control.Applicative ((<|>))
  10 import Data.Proxy
  11
  12 import Language.Symantic.Parsing
  13 import Language.Symantic.Typing.Type
  14 import Language.Symantic.Typing.Constant
  15
  16 -- * Type 'Proj_TyCon'
  17 -- | Convenient type synonym wrapping 'Proj_TyConR'
  18 -- to initiate its recursion.
  19 type Proj_TyCon cs = Proj_TyConR cs cs
  20
  21 -- | Project the 'Constraint' indexed by the given 'Type'
  22 -- onto its proof, captured by 'TyCon' when it holds.
  23 proj_TyCon
  24  :: forall src cs q.
  25     ( Proj_TyCon cs
  26     , Source src )
  27  => Type src cs q
  28  -> Maybe (TyCon q)
  29 proj_TyCon = proj_TyConR (Proxy @cs)
  30
  31 -- ** Class 'Proj_TyConR'
  32 -- | Intermediate type class to construct an instance of 'Proj_TyCon'
  33 -- from many instances of 'Proj_TyConC', one for each item of @cs@.
  34 --
  35 -- * @cs@: starting  list of /type constants/.
  36 -- * @rs@: remaining list of /type constants/.
  37 class Proj_TyConR cs rs where
  38         proj_TyConR :: Source src => Proxy rs -> Type src cs q -> Maybe (TyCon q)
  39         proj_TyConR _rs _q = Nothing
  40
  41 -- | Test whether @c@ handles the work of 'Proj_TyCon' or not,
  42 -- or recurse on @rs@, preserving the starting list of /type constants/.
  43 instance
  44  ( Proj_TyConC cs c
  45  , Proj_TyConR cs rs
  46  ) => Proj_TyConR cs (c ': rs) where
  47         proj_TyConR _rs q =
  48                 proj_TyConC (Proxy @c)  q <|>
  49                 proj_TyConR (Proxy @rs) q
  50 -- | End the recursion.
  51 instance Proj_TyConR cs '[]
  52
  53 -- ** Class 'Proj_TyConC'
  54 -- | Handle the work of 'Proj_TyCon' for a given /type constant/ @c@,
  55 -- that is: maybe it handles the given 'Constraint',
  56 -- and if so, maybe the 'Constraint' holds.
  57 class Proj_TyConC cs c where
  58         proj_TyConC :: Source src => Proxy c -> Type src cs q -> Maybe (TyCon q)
  59         proj_TyConC _c _q = Nothing
  60
  61 -- * Class '(#)'
  62 -- | 'Constraint' union.
  63 class (x, y) => x # y
  64
  65 (#)
  66  :: Source src
  67  => Inj_TyConst cs (#)
  68  => Type src cs qx
  69  -> Type src cs qy
  70  -> Type src cs (qx # qy)
  71 (#) a b = (ty @(#) `tyApp` a) `tyApp` b
  72 infixr 2 #
  73
  74 tyQual
  75  :: Source src
  76  => Proj_TyCon cs
  77  => Inj_TyConst cs (#>)
  78  => (TyCon q -> Type src cs h -> Type src cs h)
  79  -> Type src cs q
  80  -> Type src cs h
  81  -> Type src cs (q #> h)
  82 tyQual f q h =
  83         TyApp sourceLess (TyApp sourceLess (ty @(#>)) q) $
  84         case proj_TyCon q of
  85          Just Dict -> f Dict h
  86          Nothing   -> h
  87 infix 1 `tyQual`