[GHC] #15122: GHC HEAD typechecker regression

[GHC]

#15122: GHC HEAD typechecker regression
-------------------------------------+-------------------------------------
        Reporter:  fmixing           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  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):

 I took a look. Not yet complete but may help Richard.

 Analysing the program in cmmment:8.
 {{{
 foo :: (F a ~ F b) => IsStar a -> Proxy b
                    -> Proxy (F a) -> Proxy (F b)
 foo IsStar _ p = p
 }}}
 Informally we have
 {{{
  (a::k), (b::k)
  [G] F a ~ F b
  [G] k ~ *
  [W] F a ~ F b
 }}}
 The given `k ~ *` should rewrite both the given and wanted equality, which
 should allow us to prove it no problem.

 The firsts slightly surprising thing is that the data constructor `IsStar`
 binds an existential:
 {{{
 IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => IsStar @k a
 }}}
 Is this rigth?  Well, if `IsStar` had some arguments it mmight be more
 persuasive
 {{{
 data IsStar2 (a :: k) where
   IsStar2 :: a2 -> IsStar a2
 }}}
 Now
 {{{
 IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => a2 -> IsStar @k a
 }}}
 We can't have `a` on the LHS of the arrow, because it has the wrong kind.

 Here's the implication we can't solve
 {{{
  Implic {
    TcLevel = 2
    Skolems = k_a1hM[sk:2]
              (a_a1hN[sk:2] :: k_a1hM[sk:2])
              (b_a1hO[sk:2] :: k_a1hM[sk:2])
    No-eqs = False
    Status = Unsolved
    Given =
      $d~_a1hQ :: (F a_a1hN[sk:2] :: k_a1hM[sk:2])
                  ~ (F b_a1hO[sk:2] :: k_a1hM[sk:2])
    Wanted =
      WC {wc_impl =
            Implic {
              TcLevel = 3
              Skolems = a_a1hR[ssk:3]
              No-eqs = False
              Status = Unsolved
              Given =
                co_a1hS :: (k_a1hM[sk:2] :: *)            ~# (* :: *)
                co_a1hT :: (a_a1hN[sk:2] :: k_a1hM[sk:2]) ~# (a_a1hR[ssk:3]
 :: *)
              Wanted =
                WC {wc_simple =
                      [WD] hole{co_a1ig} {3}:: (F (b_a1hO[sk:2] |> co_a1hS)
 :: *)
                                               ~# (F a_a1hR[ssk:3] :: *)
 (CNonCanonical)}
              Binds = EvBindsVar<a1hV>
              a pattern with constructor: IsStar :: forall a. IsStar a,
              in an equation for `foo_a1hP' }}
 }}}
 Not yet sure why we can't solve it.

 At the crucial moment in typechecking `foo` we see this:
 {{{
   work item = [WD] hole{co_a1hU} {0}:: (F a_a1hN[sk:2] :: k_a1hM[sk:2])
                                        ~# (F b_a1hO[sk:2] :: k_a1hM[sk:2])
 (CNonCanonical)
   inerts = {Equalities: [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *)
                                           ~# (* :: *) (CTyEqCan)
                         [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] ::
 k_a1hM[sk:2])
                                           ~# (fsk_a1i2[fsk:0] ::
 k_a1hM[sk:2]) (CTyEqCan)
                         [G] co_a1i9 {1}:: (a_a1hN[sk:2] :: k_a1hM[sk:2])
                                           ~# ((a_a1hR[ssk:3] |> Sym
 co_a1hS) :: k_a1hM[sk:2]) (CTyEqCan)
             Type-function equalities = [G] co_a1ib {0}:: (F (b_a1hO[sk:2]
 |> co_a1hS) :: *)
                                                          ~#
 (fsk_a1ia[fsk:0] :: *) (CFunEqCan)
                                        [G] co_a1id {0}:: (F a_a1hR[ssk:3]
 :: *)
                                                          ~#
 (fsk_a1ic[fsk:0] :: *) (CFunEqCan)
             Dictionaries = [G] $d~~_a1i8 {0}:: ((fsk_a1i2[fsk:0] |>
 co_a1hS) :: *)
                                                ~~ ((fsk_a1i2[fsk:0] |>
 co_a1hS) :: *) (CDictCan)
                            [G] $d~_a1i7 {0}:: ((fsk_a1i2[fsk:0] |>
 co_a1hS) :: *)
                                               ~ ((fsk_a1i2[fsk:0] |>
 co_a1hS) :: *) (CDictCan)
 }}}
 Note these two lines:
 {{{
   [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *)               ~# (* :: *)
 (CTyEqCan)
   [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] :: k_a1hM[sk:2]) ~# (fsk_a1i2[fsk:0]
 :: k_a1hM[sk:2]) (CTyEqCan)
 }}}
 The first can rewrite the second, but we have not made it do so.  I think
 because the substitution does not claim to be idempotent.

 But then we end up trying to prove that
 {{{
 [W] fsk1 :: *  ~  fsk2 : *
 }}{
 and we have somehow lost the connection to our 'givens'.  That's as far as
 I got.

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