[GHC] #15870: No skolem info panic

[GHC]

#15870: No skolem info panic
-------------------------------------+-------------------------------------
        Reporter:  sheaf             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.6.3
       Component:  Compiler (Type    |              Version:  8.6.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * priority:  normal => highest
 * milestone:   => 8.6.3


Comment:

 First, this appears to be a regression from GHC 8.4, which simply gives an
 error message:

 {{{
 $ /opt/ghc/8.4.4/bin/ghci Bug.hs -XTypeInType
 GHCi, version 8.4.4: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:30:34: error:
     • Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
     • In the second argument of ‘Get’, namely ‘g2’
       In the type ‘Get a g2’
       In the type instance declaration for ‘Get’
    |
 30 |   type Get a (g1 :.: g2) = Get a g2
    |                                  ^^
 }}}

 So that's not good. I'll mark this as highest priority as a result.

 Second, the error message:

 {{{
     • Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’
     • In the second argument of ‘Gettable’, namely ‘g2’
       In the instance declaration for ‘Gettable a (g1 :.: g2)’
    |
 20 |         , Gettable b g2
    |
 }}}

 Is actually expected behavior (at least, at the moment). Even though
 you've written `b ~ Get a g1`, GHC isn't able to make use of this fact at
 the type level yet. See #12677/#15710 for the tickets tracking this
 infelicity.

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