Re: [GHC] #14887: Explicitly quantifying a kind variable causes a telescope to fail to kind-check

26 Apr 2018

      #14887: Explicitly quantifying a kind variable causes a telescope to fail to kind-
check
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's what is going on with:
 {{{
 foo2 :: forall (k :: Type) (e :: Proxy (a :: k)). Int
 }}}
 In `TcHsType.tc_hs_sig_type_and_gen` we see
 {{{
 tc_hs_sig_type_and_gen skol_info (HsIB { hsib_vars = sig_vars
                                        , hsib_body = hs_ty }) kind
   = do { (tkvs, ty) <- solveEqualities $
                        tcImplicitTKBndrs skol_info sig_vars $
                        tc_lhs_type typeLevelMode hs_ty kind
 }}}
 Here `sig_vars` is just `a`.  Now `tcImplicitTKBndrs` gives `a` a kind
 `k0` (a unification variable), so
 we attempt to kind-check
 {{{
    forall (a::k0). forall (k :: Type) (e :: Proxy (a :: k)). Int
 }}}
 But that requires `k0 ~ k`, which is a skolem-escape problem.  We end up
 trying (and failing) solve
 the constraint
 {{{
 Implic {
   TcLevel = 2
   Skolems = (a_avH[sk:2] :: k_aZs[tau:2])
   No-eqs = True
   Status = Unsolved
   Given =
   Wanted =
     WC {wc_impl =
           Implic {
             TcLevel = 3
             Skolems = k_aZp[sk:3]
                       (e_aZq[sk:3] :: Proxy
                                         k_aZp[sk:3] (a_avH[sk:2] |>
 {co_aZC}))
             No-eqs = True
             Status = Unsolved
             Given =
             Wanted =
               WC {wc_simple =
                     [WD] hole{co_aZC} {0}:: (k_aZs[tau:2] :: *)
                                             GHC.Prim.~# (k_aZp[sk:3] :: *)
 (CNonCanonical)}
 }}}
 Here `k0` is `k_aZs`, and it is (rightly) untouchable inside the level-3
 implication.
 Hence the error message.

 I have not yet thought about what to do.  Richard may have some ideas.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14887#comment:7
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler