[Haskell-cafe] Mystery: constructor type applications differ from signatures
Tom Ellis
tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk
Sat Oct 29 12:12:15 UTC 2022
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
More information about the Haskell-Cafe
mailing list