1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE KindSignatures #-}
7 {-# LANGUAGE MultiParamTypeClasses #-}
8 {-# LANGUAGE Rank2Types #-}
9 {-# LANGUAGE ScopedTypeVariables #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE TypeOperators #-}
12 {-# LANGUAGE UndecidableInstances #-}
13 module Language.Symantic.Expr.Common where
15 import Data.Proxy (Proxy(..))
16 import Data.Text (Text)
17 import qualified Data.Text as Text
18 import Data.Type.Equality ((:~:)(Refl))
19 import GHC.Prim (Constraint)
21 import Language.Symantic.Type
23 -- * Class 'Expr_from'
25 -- | Parse given @ast@ into
26 -- a 'Type_Root_of_Expr' and
27 -- a 'Forall_Repr_with_Context',
28 -- or return an 'Error_of_Expr'.
29 class Expr_from ast (ex:: *) where
30 expr_from :: Expr_From ast ex hs ret
32 -- ** Type 'Expr_From'
33 type Expr_From ast ex hs ret
35 -- ^ Select the 'Expr_from' instance.
37 -- ^ The input data to parse.
38 -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
39 -- ^ The bound variables in scope and their types:
40 -- held in the heterogeneous list @hs@,
41 -- from the closest including lambda abstraction to the farest.
43 . Type_Root_of_Expr ex h
44 -> Forall_Repr_with_Context ex hs h
45 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
46 -- ^ The accumulating continuation.
47 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
51 :: forall ty lit ex ast hs ret.
52 ( ty ~ Type_Root_of_Expr ex
54 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
55 (Error_of_Expr ast (Root_of_Expr ex))
56 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
57 -> ty lit -> Lambda_Var_Name
58 -> Expr_From ast ex hs ret
59 lit_from lit ty_lit toread ex ast _ctx k =
60 case read_safe toread of
61 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
62 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
64 -- | Parse a unary operator.
66 :: forall root ty lit ex ast hs ret.
67 ( ty ~ Type_Root_of_Expr ex
68 , root ~ Root_of_Expr ex
69 , Type_Eq (Type_Root_of_Expr root)
71 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
72 (Error_of_Expr ast root)
73 , Root_of_Expr root ~ root
74 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
76 -> Expr_From ast ex hs ret
77 op1_from op ty_lit ast_x ex ast ctx k =
78 expr_from (Proxy::Proxy root) ast_x ctx $
79 \ty_x (Forall_Repr_with_Context x) ->
80 check_type_eq ex ast ty_lit ty_x $ \Refl ->
81 k ty_x $ Forall_Repr_with_Context (op . x)
83 -- | Parse a binary operator.
85 :: forall root ty lit ex ast hs ret.
86 ( ty ~ Type_Root_of_Expr ex
87 , root ~ Root_of_Expr ex
88 , Type_Eq (Type_Root_of_Expr root)
90 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
91 (Error_of_Expr ast root)
92 , Root_of_Expr root ~ root
93 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
94 -> ty lit -> ast -> ast
95 -> Expr_From ast ex hs ret
96 op2_from op ty_lit ast_x ast_y ex ast ctx k =
97 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
98 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
99 check_type_eq ex ast ty_lit ty_x $ \Refl ->
100 check_type_eq ex ast ty_lit ty_y $ \Refl ->
101 k ty_x $ Forall_Repr_with_Context $
106 -- | GADT for a typing context,
107 -- accumulating an @item@ at each lambda;
108 -- used to accumulate object-types (in 'Expr_from')
109 -- or host-terms (in 'Repr_Host')
110 -- associated with the 'Lambda_Var's in scope.
111 data Context :: (* -> *) -> [*] -> * where
112 Context_Empty :: Context item '[]
113 Context_Next :: item h -> Context item hs -> Context item (h ': hs)
114 infixr 5 `Context_Next`
116 -- ** Type 'Lambda_Var'
117 -- | Join a name and a type.
119 -- This data type is used to handle lambda variables by name
120 -- (instead of DeBruijn indices for instance).
122 = Lambda_Var Lambda_Var_Name (ty h)
123 type Lambda_Var_Name = Text
125 -- ** Type 'Forall_Repr_with_Context'
126 -- | A data type embedding a universal quantification
127 -- over an interpreter @repr@
128 -- and qualified by the symantics of an expression.
130 -- Moreover the expression is abstracted by a 'Context'
131 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
132 -- for lambda abstractions.
134 -- This data type is used to keep a parsed expression polymorphic enough
135 -- to stay interpretable by different interpreters.
137 -- NOTE: 'Sym_of_Expr'@ ex repr@
138 -- is needed to be able to use symantic methods of the parsed expression
139 -- into a 'Forall_Repr_with_Context'@ ex@.
141 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
142 -- is needed to be able to use an expression
143 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
144 -- into a 'Forall_Repr_with_Context'@ ex@,
145 -- which happens when a symantic method includes a polymorphic type
146 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
147 data Forall_Repr_with_Context ex hs h
148 = Forall_Repr_with_Context
149 ( forall repr. ( Sym_of_Expr ex repr
150 , Sym_of_Expr (Root_of_Expr ex) repr
151 ) => Context repr hs -> repr h )
153 -- ** Type 'Forall_Repr'
154 data Forall_Repr ex h
156 { unForall_Repr :: forall repr
157 . Sym_of_Expr ex repr
160 -- ** Type family 'Root_of_Expr'
161 -- | The root expression of an expression.
162 type family Root_of_Expr (ex:: *) :: *
164 -- ** Type family 'Sym_of_Expr'
165 -- | The symantic of an expression.
166 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
168 -- ** Type family 'Error_of_Expr'
169 -- | The error(s) of an expression.
170 type family Error_of_Expr (ast:: *) (ex:: *) :: *
172 -- ** Type family 'Type_of_Expr'
173 -- | The type of an expression, parameterized by a root type.
174 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
176 -- ** Type 'Type_Root_of_Expr'
177 -- | Convenient alias.
179 -- NOTE: include 'Type_Var' only to use it
180 -- within 'Error_Expr_Type_mismatch' so far.
181 type Type_Root_of_Expr (ex:: *)
182 = Type_Root (Type_Alt Type_Var (Type_of_Expr (Root_of_Expr ex)))
184 -- * Type 'Expr_Root'
185 -- | The root expression, passing itself as parameter to the given expression.
186 newtype Expr_Root (ex:: * -> *)
187 = Expr_Root (ex (Expr_Root ex))
188 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
189 type instance Type_of_Expr (Expr_Root ex)
190 = Type_of_Expr (ex (Expr_Root ex))
191 type instance Error_of_Expr ast (Expr_Root ex)
192 = Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
193 (Type_Root_of_Expr (ex (Expr_Root ex)))
195 (Error_of_Expr ast (ex (Expr_Root ex)))
196 type instance Sym_of_Expr (Expr_Root ex) repr
197 = Sym_of_Expr (ex (Expr_Root ex)) repr
198 instance -- Expr_from
199 ( Expr_from ast (ex (Expr_Root ex))
200 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
201 ) => Expr_from ast (Expr_Root ex) where
202 expr_from _ex ctx ast k =
203 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
204 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
205 k ty (Forall_Repr_with_Context repr)
207 {- NOTE: useless code so far.
208 -- ** Class 'Expr_Root_Lift'
209 -- | Lift a given expression to a given root expression.
210 class Expr_Root_Lift ex root where
211 expr_root_lift :: ex root -> root
214 Expr_Root_Lift ex (Expr_Root root) where
215 expr_root_lift = Expr_Root . expr_lift
219 -- | Expression making an alternative between two expressions.
220 data Expr_Alt curr next (root:: *)
221 = Expr_Alt_Curr (curr root)
222 | Expr_Alt_Next (next root)
223 type instance Root_of_Expr (Expr_Alt curr next root) = root
224 type instance Sym_of_Expr (Expr_Alt curr next root) repr
225 = ( Sym_of_Expr (curr root) repr
226 , Sym_of_Expr (next root) repr
228 type instance Type_of_Expr (Expr_Alt curr next root)
229 = Type_of_Expr_Alt (Type_of_Expr (curr root))
230 (Type_of_Expr (next root))
231 -- ** Type family 'Type_of_Expr_Alt'
232 -- | Remove 'No_Type' type when building 'Type_of_Expr'.
233 type family Type_of_Expr_Alt
234 (type_curr:: (* -> *) -> * -> *)
235 (type_next:: (* -> *) -> * -> *)
237 Type_of_Expr_Alt No_Type next = next
238 Type_of_Expr_Alt curr No_Type = curr
239 Type_of_Expr_Alt curr next = Type_Alt curr next
241 type instance Error_of_Expr ast (Expr_Alt curr next root)
242 = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
243 (Error_of_Expr ast (next root))
244 -- ** Type family 'Error_of_Expr_Alt'
245 -- | Remove 'No_Error_Expr' type when building the error of an expression.
246 type family Error_of_Expr_Alt ast curr next where
247 Error_of_Expr_Alt ast No_Error_Expr next = next
248 Error_of_Expr_Alt ast curr No_Error_Expr = curr
249 Error_of_Expr_Alt ast curr next = Error_Expr_Alt curr next
251 -- ** Type 'No_Error_Expr'
252 -- | A discarded error.
257 instance -- Expr_from
258 ( Expr_from ast (curr root)
259 , Expr_from ast (next root)
260 , Root_of_Expr (curr root) ~ root
261 , Root_of_Expr (next root) ~ root
262 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
263 (Type_Root_of_Expr root) ast)
264 (Error_of_Expr ast root)
265 ) => Expr_from ast (Expr_Alt curr next root) where
266 expr_from _ex ctx ast k =
267 case expr_from (Proxy::Proxy (curr root)) ctx ast $
268 \ty (Forall_Repr_with_Context repr) ->
269 Right $ k ty (Forall_Repr_with_Context repr) of
272 case error_expr_unlift err of
273 Just (Error_Expr_Unsupported_here _
274 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
275 (Type_Root_of_Expr root) ast) ->
276 expr_from (Proxy::Proxy (next root)) ctx ast $
277 \ty (Forall_Repr_with_Context repr) ->
278 k ty (Forall_Repr_with_Context repr)
281 {- NOTE: useless code so far.
282 -- ** Type 'Expr_Lift'
283 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
284 type Expr_Lift ex exs
285 = Expr_LiftN (Peano_of_Expr ex exs) ex exs
287 -- | Convenient wrapper around 'expr_liftN',
288 -- passing it the 'Peano' number from 'Peano_of_Expr'.
290 :: forall ex exs (root:: *).
293 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
295 -- *** Type family 'Peano_of_Expr'
296 -- | Return a 'Peano' number derived from the location
297 -- of a given expression within a given expression stack,
298 -- which is used to avoid @OverlappingInstances@.
299 type family Peano_of_Expr
301 (exs:: * -> *) :: * where
302 Peano_of_Expr ex ex = Zero
303 Peano_of_Expr ex (Expr_Alt ex next) = Zero
304 Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)
306 -- *** Class 'Expr_LiftN'
307 -- | Lift a given expression to the top of a given expression stack including it,
308 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
309 class Expr_LiftN (p:: *) ex exs where
310 expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
311 instance Expr_LiftN Zero curr curr where
313 instance Expr_LiftN Zero curr (Expr_Alt curr next) where
314 expr_liftN _ = Expr_Alt_Curr
316 Expr_LiftN p other next =>
317 Expr_LiftN (Succ p) other (Expr_Alt curr next) where
318 expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)
320 -- ** Type 'Expr_Unlift'
321 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
322 type Expr_Unlift ex exs
323 = Expr_UnliftN (Peano_of_Expr ex exs) ex exs
325 -- | Convenient wrapper around 'expr_unliftN',
326 -- passing it the 'Peano' number from 'Peano_of_Expr'.
328 :: forall ex exs (root:: *).
329 Expr_Unlift ex exs =>
330 exs root -> Maybe (ex root)
331 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
333 -- *** Class 'Expr_UnliftN'
334 -- | Try to unlift a given expression out of a given expression stack including it,
335 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
336 class Expr_UnliftN (p:: *) ex exs where
337 expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
338 instance Expr_UnliftN Zero curr curr where
339 expr_unliftN _ = Just
340 instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
341 expr_unliftN _ (Expr_Alt_Curr x) = Just x
342 expr_unliftN _ (Expr_Alt_Next _) = Nothing
344 Expr_UnliftN p other next =>
345 Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
346 expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
347 expr_unliftN _ (Expr_Alt_Curr _) = Nothing
350 -- ** Type family 'Is_Last_Expr'
351 -- | Return whether a given expression is the last one in a given expression stack.
353 -- NOTE: each expression parser uses this type family
354 -- when it encounters unsupported syntax:
355 -- to know if it is the last expression parser component that will be tried
356 -- (and thus return 'Error_Expr_Unsupported')
357 -- or if some other expression parser component shall be tried
358 -- (and thus return 'Error_Expr_Unsupported_here',
359 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
360 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
361 Is_Last_Expr ex ex = 'True
362 Is_Last_Expr ex (Expr_Root exs) = Is_Last_Expr ex (exs (Expr_Root exs))
363 Is_Last_Expr (ex root) (Expr_Alt ex next root) = 'False
364 Is_Last_Expr other (Expr_Alt curr next root) = Is_Last_Expr other (next root)
366 -- * Type 'Error_Expr_Alt'
367 -- | Error expression making an alternative between two error expressions.
368 data Error_Expr_Alt curr next
369 = Error_Expr_Alt_Curr curr
370 | Error_Expr_Alt_Next next
373 -- ** Type 'Error_Expr_Lift'
374 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
375 type Error_Expr_Lift err errs
376 = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
378 -- | Convenient wrapper around 'error_expr_liftN',
379 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
382 Error_Expr_Lift err errs => err -> errs
383 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
385 -- *** Type family 'Peano_of_Error_Expr'
386 -- | Return a 'Peano' number derived from the location
387 -- of a given error expression within a given error expression stack,
388 -- which is used to avoid @OverlappingInstances@.
389 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
390 Peano_of_Error_Expr err err = Zero
391 Peano_of_Error_Expr err (Error_Expr_Alt err next) = Zero
392 Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
394 -- *** Class 'Error_Expr_LiftN'
395 -- | Lift a given expression to the top of a given expression stack including it,
396 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
397 class Error_Expr_LiftN (p:: *) err errs where
398 error_expr_liftN :: Proxy p -> err -> errs
399 instance Error_Expr_LiftN Zero curr curr where
400 error_expr_liftN _ = id
401 instance Error_Expr_LiftN Zero curr (Error_Expr_Alt curr next) where
402 error_expr_liftN _ = Error_Expr_Alt_Curr
404 Error_Expr_LiftN p other next =>
405 Error_Expr_LiftN (Succ p) other (Error_Expr_Alt curr next) where
406 error_expr_liftN _ = Error_Expr_Alt_Next . error_expr_liftN (Proxy::Proxy p)
408 -- ** Type 'Error_Expr_Unlift'
409 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
410 type Error_Expr_Unlift ex exs
411 = Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
413 -- | Convenient wrapper around 'error_expr_unliftN',
414 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
417 Error_Expr_Unlift ex exs => exs -> Maybe ex
418 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
420 -- *** Class 'Error_Expr_UnliftN'
421 -- | Try to unlift a given expression error out of a given expression error stack including it,
422 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
423 class Error_Expr_UnliftN (p:: *) ex exs where
424 error_expr_unliftN :: Proxy p -> exs -> Maybe ex
425 instance Error_Expr_UnliftN Zero curr curr where
426 error_expr_unliftN _ = Just
427 instance Error_Expr_UnliftN Zero curr (Error_Expr_Alt curr next) where
428 error_expr_unliftN _ (Error_Expr_Alt_Curr x) = Just x
429 error_expr_unliftN _ (Error_Expr_Alt_Next _) = Nothing
431 Error_Expr_UnliftN p other next =>
432 Error_Expr_UnliftN (Succ p) other (Error_Expr_Alt curr next) where
433 error_expr_unliftN _ (Error_Expr_Alt_Next x) = error_expr_unliftN (Proxy::Proxy p) x
434 error_expr_unliftN _ (Error_Expr_Alt_Curr _) = Nothing
436 -- * Type 'Error_Expr_Read'
437 -- | Common expression errors.
438 data Error_Expr err_ty ty ast
439 = Error_Expr_Wrong_number_of_arguments ast Int
440 -- ^ Wrong number of arguments applied to a term,
441 -- the integer is the number of arguments expected.
442 | Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
443 -- ^ Mismatch between respectively expected and actual type.
444 | Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
445 -- ^ A 'Constraint' is missing.
446 | Error_Expr_Read Error_Read ast
447 -- ^ Error when reading a literal.
448 | Error_Expr_Type err_ty ast
449 -- ^ Error when parsing a type.
450 | Error_Expr_Unsupported ast
451 -- ^ Given syntax is supported by none
452 -- of the expression parser components
453 -- of the expression stack.
454 | Error_Expr_Unsupported_here ast
455 -- ^ Given syntax not supported by
456 -- the current expression parser component.
459 -- | Convenient wrapper around 'error_expr_lift',
460 -- passing the type family boilerplate.
463 (ty ~ Type_Root_of_Expr ex)
465 (Error_Expr (Error_of_Type ast ty) ty ast)
466 (Error_of_Expr ast (Root_of_Expr ex))
468 -> Error_Expr (Error_of_Type ast ty) ty ast
469 -> Error_of_Expr ast (Root_of_Expr ex)
470 error_expr _ = error_expr_lift
472 -- | Parsing utility to return 'Error_Expr_Unsupported'
473 -- or 'Error_Expr_Unsupported_here'
474 -- according to the given expression.
475 error_expr_unsupported
476 :: forall ast ex ty root.
477 ( root ~ Root_of_Expr ex
478 , ty ~ Type_Root_of_Expr ex
479 , Implicit_HBool (Is_Last_Expr ex root)
480 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
481 (Error_of_Expr ast root)
483 -> Error_of_Expr ast (Root_of_Expr ex)
484 error_expr_unsupported ex ast =
485 case hbool :: HBool (Is_Last_Expr ex root) of
486 HTrue -> error_expr ex $ Error_Expr_Unsupported ast
487 HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
489 -- | Parsing utility to check that two types are equal,
490 -- or raise 'Error_Expr_Type_mismatch'.
492 :: forall ast ex root ty x y ret.
493 ( root ~ Root_of_Expr ex
494 , ty ~ Type_Root_of_Expr ex
496 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
497 (Error_of_Expr ast root)
499 => Proxy ex -> ast -> ty x -> ty y
500 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
501 -> Either (Error_of_Expr ast root) ret
502 check_type_eq ex ast x y k =
503 case x `type_eq` y of
505 Nothing -> Left $ error_expr ex $
506 Error_Expr_Type_mismatch ast
510 -- | Parsing utility to check that a type is has instance of a given 'Constraint',
511 -- or raise 'Error_Expr_Constraint_missing'.
512 check_type_constraint
513 :: forall ast ex c root ty h ret.
514 ( root ~ Root_of_Expr ex
515 , ty ~ Type_Root_of_Expr ex
516 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
517 (Error_of_Expr ast root)
518 , Type_Constraint c ty
520 => Proxy ex -> Proxy c -> ast -> ty h
521 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
522 -> Either (Error_of_Expr ast root) ret
523 check_type_constraint ex c ast ty k =
524 case type_constraint c ty of
526 Nothing -> Left $ error_expr ex $
527 Error_Expr_Constraint_missing ast
529 -- FIXME: not easy to report the constraint
530 -- and still support 'Eq' and 'Show' deriving.
533 -- * Type 'Error_Read'
534 -- | Error parsing a host-term.
539 -- | Parse a host-term.
540 read_safe :: Read h => Text -> Either Error_Read h
542 case reads $ Text.unpack t of
544 _ -> Left $ Error_Read t