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 'TyCon'
  17 -- | Captures the proof of a 'Constraint'
  18 -- (and its dictionaries when it contains type classes):
  19 -- pattern matching on the 'Dict' constructor
  20 -- brings the 'Constraint' into scope.
  21 data TyCon c where
  22         Dict :: c => TyCon c
  23
  24 -- * Type 'Proj_TyCon'
  25 -- | Convenient type synonym wrapping 'Proj_TyConR'
  26 -- to initiate its recursion.
  27 type Proj_TyCon cs = Proj_TyConR cs cs
  28
  29 -- | Project the 'Constraint' indexed by the given 'Type'
  30 -- onto its proof, captured by 'TyCon' when it holds.
  31 proj_TyCon
  32  :: forall src ctx ss cs q.
  33     Source src
  34  => Proj_TyCon cs
  35  => Type src ctx ss 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 :: Source src => Proxy rs -> Type src ctx ss 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 (Proxy 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 :: Source src => Proxy c -> Type src ctx ss cs q -> Maybe (TyCon q)
  67         proj_TyConC _c _q = Nothing
  68
  69 -- * Class @(#)@
  70 -- | 'Constraint' union.
  71 class (x, y) => x # y
  72
  73 (#) :: Source src
  74     => Inj_TyConst cs (#)
  75     => Type src ctx ss cs qx
  76     -> Type src ctx ss cs qy
  77     -> Type src ctx ss cs (qx # qy)
  78 (#) a b = (ty @(#) `tyApp` a) `tyApp` b
  79 infixr 2 #
  80
  81 instance Fixity_TyConstC (#) where
  82         fixity_TyConstC _ = FixityInfix $ infixB L 0
  83
  84 tyQual
  85  :: Source src
  86  => Proj_TyCon cs
  87  => Inj_TyConst cs (#>)
  88  => Type src ctx ss cs q
  89  -> Type src ctx ss cs h
  90  -> (TyCon q -> Type src ctx ss cs h -> Type src ctx ss cs h)
  91  -> Type src ctx ss cs (q #> h)
  92 tyQual q h f =
  93         TyApp sourceLess (TyApp sourceLess (ty @(#>)) q) $
  94         case proj_TyCon q of
  95          Just Dict -> f Dict h
  96          Nothing   -> h
  97 infix 1 `tyQual`