]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Constraint.hs
Rename grammar rules, prefixing them with g_.
[haskell/symantic.git] / 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