[Haskell-cafe] Mystery: constructor type applications differ from signatures

[Tom Ellis]

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-1295488553)

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 at .
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 at .
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 at .
data FunRep a where
  AppK ::
    forall k (b :: k).
    IsType k ->
    Proxy k ->
    FunRep b

-- | @IsType k@ witnesses that @k ~ Type at .
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