Looping dynApply

[goldfirere]

The following loops

{-# 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 :: k1) 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

dynApply :: Dyn -> Dyn -> Maybe Dyn
dynApply (Dyn (TyApp (TyApp (TyCon tarrow) targ) tres) fun) (Dyn targ' arg)
  = case (eqTc tarrow TArrow, eqT targ targ') of
      (Just Refl, Just Refl)  -> Just (Dyn tres (fun arg))
      _    -> Nothing
dynApply _ _ = Nothing