{-# 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 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
Errors
Scratch.hs:57:31:
Could not deduce (k3 ~ *)
from the context (* GHC.Prim.~# k2, a5 GHC.Prim.~# b2)
bound by a pattern with constructor
Refl :: forall t_a1Xh (a :: t_a1Xh). a :~: a,
in a case alternative
at Scratch.hs:57:12-15
‘k3’ is a rigid type variable bound by
a pattern with pattern synonym
Arrow :: forall k_a23b (t_a23c :: k_a23b) k (a :: k
-> k_a23b) (b :: k) (gadt_a23g :: t_a23c
GHC.Prim.~# a b) k (a :: k
-> k
-> k_a23b) (b :: k) (gadt_a23k :: a
GHC.Prim.~# a b) (gadt_a23y :: (k
-> k
-> k_a23b)
GHC.Prim.~# (*
-> *
-> *)) (gadt_a23z :: a
GHC.Prim.~# (->)).
TypeRep b -> TypeRep b -> TypeRep t_a23c,
in an equation for ‘dynApply’
at Scratch.hs:55:16
Expected type: TypeRep (b3 |> Sub _cobox)
Actual type: TypeRep b3
which classifies: tres
Relevant bindings include
tres :: TypeRep b3 (bound at Scratch.hs:55:27)
In the first argument of ‘Dyn’, namely ‘tres’
In the first argument of ‘Just’, namely ‘(Dyn tres (fun arg))’
Scratch.hs:57:37:
Could not deduce (a2 ~ ((b2 |> Sym _cobox1) -> (b3 |> Sub _cobox)))
from the context (* GHC.Prim.~# k2, a5 GHC.Prim.~# b2)
bound by a pattern with constructor
Refl :: forall t_a1Xh (a :: t_a1Xh). a :~: a,
in a case alternative
at Scratch.hs:57:12-15
‘a2’ is a rigid type variable bound by
a pattern with constructor
Dyn :: forall a. TypeRep a -> a -> Dyn,
in an equation for ‘dynApply’
at Scratch.hs:55:11
Expected type: a5 -> (b3 |> Sub _cobox)
Actual type: a2
Relevant bindings include
fun :: a2 (bound at Scratch.hs:55:33)
tres :: TypeRep b3 (bound at Scratch.hs:55:27)
targ :: TypeRep b2 (bound at Scratch.hs:55:22)
The function ‘fun’ is applied to one argument,
but its type ‘a2’ has none
In the second argument of ‘Dyn’, namely ‘(fun arg)’
In the first argument of ‘Just’, namely ‘(Dyn tres (fun arg))’
Failed, modules loaded: none.
Prelude>
Note that there is some tidying in the first error message, but some bound variables are printed with the same names! And, are these errors at all appropriate?
Code:
Errors
Note that there is some tidying in the first error message, but some bound variables are printed with the same names! And, are these errors at all appropriate?