Re: [GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

13 Oct 2017

      #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Another program with a similar structure and error message:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind

 data Proxy a = Proxy
 data family Sing (a :: k)

 data SomeSing k where
   SomeSing :: Sing (a :: k) -> SomeSing k

 class SingKind k where
   type Demote k :: Type
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k

 data instance Sing (x :: Proxy k) where
   SProxy :: forall (a :: k). Sing ('Proxy :: Proxy a)

 instance SingKind (Proxy k) where
   type Demote (Proxy k) = Proxy k
   fromSing SProxy = Proxy
   toSing Proxy = SomeSing SProxy

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type a @@ b = Apply a b
 infixl 9 @@

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }

 instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
   type Demote (k1 ~> k2) = Demote k1 -> Demote k2
   fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing
 sFun y)
   toSing = undefined

 dapp :: forall (a :: Type)
                (f :: forall (x :: a). Proxy x ~> Type)
                (x :: a).
         Sing f
      -> Sing x
      -> f @@ ('Proxy :: Proxy x)
 dapp f x = case f of
             SLambda (sF :: _) -> undefined
 }}}

 This time, all GHCs from 8.0.1 on give a similar panic:

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

 Bug.hs:56:28: error:
     • Found type wildcard ‘_’
         standing for ‘Singghc: panic! (the 'impossible' happened)
   (GHC version 8.2.1 for x86_64-unknown-linux):
         No skolem info:
   a1_a1tE[sk:1]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in
 ghc:TcErrors
 }}}

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