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

27 Jul 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       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies,                      |
  PartialTypeSignatures              |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13877
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 (Originally spun off from #13877.)

 The following program gives a somewhat decent error message in GHC 8.0.1:

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

 import Data.Kind

 data family Sing (a :: k)

 data WeirdList :: Type -> Type where
   WeirdNil  :: WeirdList a
   WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a

 data instance Sing (z :: WeirdList a) where
   SWeirdNil  :: Sing WeirdNil
   SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)

 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
                         (p :: forall (x :: Type). x -> WeirdList x ->
 Type).
                  Sing wl
               -> (forall (y :: Type). p _ WeirdNil)
               -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList
 z)).
                     Sing x -> Sing xs -> p _ xs
                   -> p _ (WeirdCons x xs))
               -> p _ wl
 elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
 elimWeirdList (SWeirdCons (x :: Sing (x :: z))
                           (xs :: Sing (xs :: WeirdList (WeirdList z))))
               pWeirdNil pWeirdCons
   = pWeirdCons @z @x @xs x xs
       (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
 }}}

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

 Foo.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
                                        -> (forall y. p x0 t3 'WeirdNil)
                                        -> (forall z (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                            Sing x
                                            -> Sing xs
                                            -> p (WeirdList z) t2 xs
                                            -> p z t1 ('WeirdCons x xs))
                                        -> p a t0 wl’
       to a visible type argument ‘WeirdList z’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
       In the expression:
         pWeirdCons
           @z
           @x
           @xs
           x
           xs
           (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
       In an equation for ‘elimWeirdList’:
           elimWeirdList
             (SWeirdCons (x :: Sing (x :: z))
                         (xs :: Sing (xs :: WeirdList (WeirdList z))))
             pWeirdNil
             pWeirdCons
             = pWeirdCons
                 @z
                 @x
                 @xs
                 x
                 xs
                 (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil
 pWeirdCons)
 }}}

 But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:

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

 Foo.hs:24:41: error:
     • Found type wildcard ‘_’ standing for ‘t0’
       Where: ‘t0’ is an ambiguous type variable
              ‘x0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
     • Relevant bindings include
         elimWeirdList :: Sing wl
                          -> (forall y. p x0 t0 'WeirdNil)
                          -> (forall z (x :: z) (xs :: WeirdList (WeirdList
 z)).
                              Sing x
                              -> Sing xs -> p (WeirdList z) t1 xs -> p z t2
 ('WeirdCons x xs))
                          -> p a t3 wl
           (bound at Foo.hs:29:1)

 Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
   (GHC version 8.0.2 for x86_64-unknown-linux):
         No skolem info: z_a13X[sk]
 }}}

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Foo.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              ( Foo.hs, interpreted )

 Foo.hs:21:18: error:
     • The kind of variable ‘wl1’, namely ‘WeirdList a1’,
       depends on variable ‘a1’ from an inner scope
       Perhaps bind ‘wl1’ sometime after binding ‘a1’
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 Foo.hs:24:41: error:
     • Found type wildcard ‘_’ standing for ‘w0’
       Where: ‘w0’ is an ambiguous type variable
              ‘x0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 24 |               -> (forall (y :: Type). p _ WeirdNil)
    |                                         ^

 Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.1 for x86_64-unknown-linux):
         No skolem info:
   z_a1sY[sk:2]
   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
 }}}

 (The error messages from HEAD, at commit
 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)

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