[GHC] #11506: uType_defer can defer too long

[GHC]

#11506: uType_defer can defer too long
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11506>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler