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