blob: 2bd6b74e44736e774e7b3268eb4654306c9f8629 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
{-# LANGUAGE GADTs, ExistentialQuantification, KindSignatures, RankNTypes #-}
-- Succeeds (needs the (Ord a) in TypeSet
-- c.f. gadt21.hs
-- However, it's a useful test because it unearthed a bug
-- in free-variable-finding
module Expr where
import qualified Data.Kind as K (Type)
import Data.Set (Set)
data Type a where
TypeInt :: Type Int
TypeSet :: Ord a => Type a -> Type (Set a)
TypeFun :: Type a -> Type b -> Type (a -> b)
data Expr :: K.Type -> K.Type where
Const :: Type a -> a -> Expr a
data DynExpr = forall a. DynExpr (Expr a)
withOrdDynExpr :: DynExpr -> (forall a. Ord a => Expr a -> b) -> Maybe b
withOrdDynExpr (DynExpr e@(Const (TypeSet _) _)) f = Just (f e)
withOrdDynExpr (DynExpr e@(Const TypeInt _)) f = Just (f e)
withOrdDynExpr _ _ = Nothing
|
