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