[GHC] #15870: No skolem info panic

[GHC]

#15870: No skolem info panic
-------------------------------------+-------------------------------------
           Reporter:  sheaf          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.2
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 I've been toying with some type-level lenses and running into some issues
 with kind unification, when I ran into a panic:


 {{{
 bug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)
   (GHC version 8.6.2 for x86_64-unknown-mingw32):
         No skolem info:
   [k_a1Hgj]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler\utils\Outputable.hs:1160:37 in
 ghc:Outputable
         pprPanic, called at compiler\\typecheck\\TcErrors.hs:2891:5 in
 ghc:TcErrors
 }}}

 Here's a boiled down version (with a bit of extraneous code left in for
 context, as it's so short):
 {{{#!hs
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
 {-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE TypeOperators          #-}

 data Optic a where
   --Index :: Nat    -> Optic a
   --Name  :: Symbol -> Optic a
   (:.:) :: Optic a -> Optic b -> Optic a -- composition

 class Gettable a (optic :: Optic a) where
   type Get a (optic :: Optic a)

 {-
 some basic instances, e.g.
 instance Gettable (a,b) (Index 0) where
   type Get (a,b) (Index 0) = a
 ...
 -}

 instance forall a b (g1 :: Optic a) (g2 :: Optic b).
         ( Gettable a g1
         , b ~ Get a g1
         , Gettable b g2
         ) => Gettable a (g1 :.: g2) where
   type Get a (g1 :.: g2) = Get a g2
 }}}

 The program I am actually trying to write has the instance declaration
 changed to
 {{{#!hs
 instance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).
         ( Gettable a g1
         , b ~ Get a g1
         , Gettable b g2
         ) => Gettable a (g1 :.: g2) where
   type Get a (g1 :.: g2) = Get (Get a g1) g2
 }}}
 but GHC complains that it can't match kinds:

 {{{
     • 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
    |
 }}}
 I don't know if there is a way around that, and I'd be interested to hear
 any advice.

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