{-# LANGUAGE DeriveDataTypeable, TypeFamilies, TemplateHaskell, DataKinds,
PolyKinds, GADTs, RankNTypes, MultiParamTypeClasses,
FlexibleInstances, UndecidableInstances,
FunctionalDependencies, StandaloneDeriving,
TypeOperators, ScopedTypeVariables, NoMonomorphismRestriction,
MonadComprehensions, DeriveGeneric, FlexibleContexts,
GeneralizedNewtypeDeriving, ConstraintKinds,
LambdaCase, ViewPatterns, AllowAmbiguousTypes,
DefaultSignatures, -- ImpredicativeTypes,
ImplicitParams, MagicHash, UnboxedTuples,
ExtendedDefaultRules, PatternSynonyms,
DeriveFunctor, OverloadedLists -- , OverlappingInstances,
-- NullaryTypeClasses
#-}
module Scratch where
data (a :: k1) :~: (b :: k2) where
Refl :: a :~: a
data TyCon (a :: k) where
TInt :: TyCon Int
TBool :: TyCon Bool
TMaybe :: TyCon Maybe
TArrow :: TyCon (->)
data TypeRep (a :: k) where
TyCon :: TyCon a -> TypeRep a
TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
eqTc :: TyCon a -> TyCon b -> Maybe (a :~: b)
eqTc TInt TInt = Just Refl
eqTc TBool TBool = Just Refl
eqTc TMaybe TMaybe = Just Refl
eqTc TArrow TArrow = Just Refl
eqTc _ _ = Nothing
eqT :: TypeRep a -> TypeRep b -> Maybe (a :~: b)
eqT (TyCon t1) (TyCon t2) = eqTc t1 t2
eqT (TyApp a1 b1) (TyApp a2 b2)
| Just Refl <- eqT a1 a2
, Just Refl <- eqT b1 b2
= Just Refl
eqT _ _ = Nothing
data Dyn where
Dyn :: TypeRep a -> a -> Dyn
pattern Arrow :: ((a -> b) ~ c) => TypeRep a -> TypeRep b -> TypeRep c
pattern Arrow arg res <- TyApp (TyApp (TyCon (eqTc TArrow -> Just Refl)) res) arg
dynApply :: Dyn -> Dyn -> Maybe Dyn
dynApply (Dyn (Arrow targ tres) fun) (Dyn targ' arg)
= case eqT targ targ' of
Just Refl -> Just (Dyn tres (fun arg))
_ -> Nothing
dynApply _ _ = Nothing
Error
Prelude> :r
[1 of 1] Compiling Scratch ( Scratch.hs, interpreted )
Scratch.hs:53:9:
Couldn't match type ‘c’
with ‘(b2 |> Sub _cobox) -> (b3 |> Sub _cobox1)’
because type variables ‘k2’, ‘b2’, ‘k3’, ‘b3’
would escape their scope
These (rigid, skolem) type variables are bound by
the type signature for
Arrow :: TypeRep a4 -> TypeRep b4 -> TypeRep c
at Scratch.hs:53:9-13
Failed, modules loaded: none.
Prelude>
Error