uType_defer can defer too long
Here is the test case:
{-# LANGUAGE PolyKinds, ExistentialQuantification, ScopedTypeVariables,
TypeFamilies, TypeInType #-}
module Bug where
import Data.Proxy
import Data.Kind
type family ProxyType where ProxyType = (Proxy :: Type -> Type)
data T = forall a. MkT (ProxyType a)
foo (MkT (_ :: Proxy a)) = const True (undefined :: a)
This should be accepted. But I get
Bug.hs:13:53: error:
• Expected a type, but ‘a’ has kind ‘k10’
• In an expression type signature: a
In the second argument of ‘const’, namely ‘(undefined :: a)’
In the expression: const True (undefined :: a)
Why should it be accepted? GHC can infer that the existential a
in MkT
has kind Type
. (Indeed this works.) Then, we should unify the pattern signature Proxy k1 a1
with ProxyType a2
; the latter expands to Proxy Type a2
and we get k1 := Type
and a1 := a2
, allowing undefined :: a
to be accepted.
Why doesn't it work? When checking the pattern type signature in foo
, GHC then checks if ProxyType a2
is a subtype of Proxy k1 a1
. This check is deferred because of the type family. In a short while, GHC needs to know that a
has kind Type
to make sure that undefined :: a
is well-typed. At this point, it doesn't know that a
has kind Type
(because the unification was deferred), and so an error is issued.
I'm not sure how to resolve this. This is indeed a consequence of TypeInType
, but it seems more to do with solver engineering than the new TypeInType
stuff. And there is an easy workaround: just add a kind signature.
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |