I can't understand the different results from three versions of almost exactly the same function. The only difference is whether I bind type variables using type application or with a type signature. In each function isMaybeF, isMaybeG and isMaybeH below I bind three type variables f, g and h: AppK @_ @f @_ t (Proxy @g :: Proxy h) f, g and h ought to be just three different ways of binding exactly the same type. To my surpise, using them gives different results. The only difference between isMaybeF, isMaybeG and isMaybeH is the type variable I apply to `FromType`. I get a type error when I use a variable that was bound by a type application (f or g). The variable that was bound by a type signature (h) works as expected. It seems that when using f or g the type checker is too eager and looks at `FromType @f` (respectively g), decides that f must be of the form `Type -> Type`, a constraint which it can't satisfy at the site of the `AppK` pattern match, so it fails. When using h, by contrast, it seems to be able to wait to dispatch that constraint until it has seen `IsType`. Subsequently I discovered a simpler example with similar behaviour, except the type checker succeeds for g as well as h. What is going on here? (This all originally arose from my investigations into https://github.com/haskell/core-libraries-committee/issues/99#issuecomment-1...) Tom {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} -- | Requires GHC >= 9.2 and the issue appears in both 9.2 and 9.4 module Puzzle where import Data.Kind (Type) import Data.Typeable (eqT, Proxy(Proxy)) import Type.Reflection (Typeable, (:~:) (Refl)) -- | @FunRep (f b)@ witnesses that @b :: Type@. data FunRep a where AppK :: forall (k :: Type) (f :: k -> Type) (b :: k). IsType k -> Proxy f -> FunRep (f b) -- | @IsType k@ witnesses that @k ~ Type@. data IsType k where IsType :: IsType Type data FromType where FromType :: forall (f :: Type -> Type). FromType -- Could not deduce: k ~ * isMaybeF :: forall (a :: Type). FunRep a -> FromType isMaybeF = \case AppK @_ @f @_ t (Proxy @g :: Proxy h) -> case t of IsType -> FromType @f -- Could not deduce: k ~ * isMaybeG :: forall (a :: Type). FunRep a -> FromType isMaybeG = \case AppK @_ @f @_ t (Proxy @_ @g :: Proxy h) -> case t of IsType -> FromType @g -- Works fine isMaybeH :: forall (a :: Type). FunRep a -> FromType isMaybeH = \case AppK @_ @f @_ t (Proxy @_ @g :: Proxy h) -> case t of IsType -> FromType @h {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} -- | Requires GHC >= 9.2 and the issue appears in both 9.2 and 9.4 module Puzzle2 where import Data.Kind (Type) import Data.Typeable (eqT, Proxy(Proxy)) import Type.Reflection (Typeable, (:~:) (Refl)) -- | @FunRep (f b)@ witnesses that @b :: Type@. data FunRep a where AppK :: forall k (b :: k). IsType k -> Proxy k -> FunRep b -- | @IsType k@ witnesses that @k ~ Type@. data IsType k where IsType :: IsType Type data FromType where FromType :: forall (b :: Type). FromType -- Works fine isMaybeF :: forall k (a :: k). FunRep a -> FromType isMaybeF = \case AppK @_ @f t (Proxy @_ @g :: Proxy h) -> case t of IsType -> FromType @f -- Works fine isMaybeG :: forall k (a :: k). FunRep a -> FromType isMaybeG = \case AppK @_ @f t (Proxy @_ @g :: Proxy h) -> case t of IsType -> FromType @g -- Works fine isMaybeH :: forall k (a :: k). FunRep a -> FromType isMaybeH = \case AppK @_ @f t (Proxy @_ @g :: Proxy h) -> case t of IsType -> FromType @h