[GHC] #15170: GHC HEAD panic (dischargeFmv)

[GHC]

#15170: GHC HEAD panic (dischargeFmv)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:  fixed             |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:
  crash or panic                     |  polykinds/T15170
      Blocked By:                    |             Blocking:
 Related Tickets:  #14880, #15076    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => closed
 * resolution:   => fixed
 * related:   => #14880, #15076


Comment:

 Thanks, Simon!

 Ironically, I was writing this to work around #14880/#15076, and while I
 applied the workaround to `f`, I forgot to apply it to `g`. This is the
 function that I //meant// to write:

 {{{#!hs
 dcomp :: forall (a :: Type)
                 (b :: a ~> Type)
                 (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~>
 c @@ ('Proxy :: Proxy x) @@ y)
                 (g :: forall (x :: a). Proxy x ~> b @@ x)
                 (x :: a).
          SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
       => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy
 xx) @@ ('Proxy :: Proxy yy)))
       -> (forall (xx :: a). Sing (g @@ ('Proxy :: Proxy xx)))
       -> Sing a
       -> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
 dcomp _sf _ _ = undefined
 }}}

 And after your most recent patch, this compiles without a hitch, even with
 `-dcore-lint`! I think we can close this in favor of #14880/#15076, as the
 Core Lint error in the original program is just a dressed-up version of
 the program in #15076.

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