Opened 2 months ago

Last modified 3 weeks ago

#15076 new bug

Typed hole with higher-rank kind causes GHC to panic (No skolem info)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.2.2
Keywords: TypedHoles, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: #14040, #14880 Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

foo :: forall (a :: Type)
              (f :: forall (x :: a). Proxy x -> Type).
       Proxy f -> ()
foo (_ :: _) = ()
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:11: error:ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180420 for x86_64-unknown-linux):
        No skolem info:
  [a_aZo[sk:1]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors

Change History (7)

comment:1 Changed 2 months ago by RyanGlScott

Echoing simonpj's comments in https://ghc.haskell.org/trac/ghc/ticket/14040#comment:7, we can see from -ddump-tc-trace that:

reportUnsolved (after zonking):
  Free tyvars: a_aZo[sk:1]
  Tidy env: ([ESf6X :-> 1], [aZo :-> a_aZo[sk:1]])
  Wanted: WC {wc_impl =
                Implic {
                  TcLevel = 2
                  Skolems = (x_a1oX[sk:2] :: a_aZo[sk:1])
                            a_a1oY[sk:2]
                            (f_a1oZ[sk:2] :: forall (x :: a_a1oY[sk:2]). Proxy x -> *)
                  No-eqs = True
                  Status = Unsolved
                  Given =
                  Wanted =
                    WC {wc_simple =
                          [D] _ {0}:: Proxy
                                        (f_a1oZ[sk:2] x_a1oX[sk:2]) (CHoleCan: TypeHole(_))}
                  Binds = EvBindsVar<a1p6>
                  Needed inner = []
                  Needed outer = []
                  the type signature for:
                    foo :: forall (x :: a_aZo[sk:1]) a (f :: forall (x :: a).
                                                             Proxy x -> *).
                           Proxy (f x) -> () }}

Here, a_aZo is not bound by any implication.

Last edited 2 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 2 months ago by RyanGlScott

Description: modified (diff)

comment:3 Changed 2 months ago by RyanGlScott

Description: modified (diff)
Summary: Typed hole causes GHC to panic (No skolem info)Typed hole with higher-rank kind causes GHC to panic (No skolem info)

comment:4 Changed 2 months ago by RyanGlScott

comment:5 Changed 2 months ago by RyanGlScott

If you don't use a typed hole:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

foo :: forall (a :: Type)
              (f :: forall (x :: a). Proxy x -> Type).
       Proxy f -> ()
foo _ = ()

Then it compiles. However, it fails with a Core Lint error:

$ /opt/ghc/8.4.2/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the type ‘forall (x :: a) a (f :: forall (x :: a).
                                         Proxy x -> *).
                 Proxy (f x) -> ()’
    @ a_aZi[sk:1] is out of scope
*** Offending Program ***
foo
  :: forall (x :: a) a (f :: forall (x :: a). Proxy x -> *).
     Proxy (f x) -> ()
[LclIdX]
foo
  = \ (@ (x_a1e5 :: a_aZi[sk:1]))
      (@ a_a1e6)
      (@ (f_a1e7 :: forall (x :: a). Proxy x -> *))
      _ [Occ=Dead] ->
      ()

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)

*** End of Offense ***


<no location info>: error: 
Compilation had errors

comment:6 Changed 8 weeks ago by simonpj

This is another example of #14880

The problem in comment:5 comes because when we kind-check foo's type signature, we generate this:

foo :: forall {xx :: a}.
       forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type)
       Proxy @(Proxy @a xx -> Type)
             (f @xx)
       -> ()

Note that the f in Proxy f gets elaborated to Proxy @.. (f @xx); that is f is instantiated with a fresh unification variable xx.

But now we kind-generalise the result and put xx at the front. But xx's kind mentions a -- disaster.

Solution proposed for #14880: do not generalise over xx; instead default it to Any. So we'd get

foo :: forall {xx :: a}.
       forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type)
       Proxy @(Proxy @a (Any a) -> Type)
             (f @(Any a))
       -> ()

which is probably fine.

comment:7 Changed 3 weeks ago by RyanGlScott

Another example of this bug, discovered in https://github.com/goldfirere/ghc/issues/57 :

{-# LANGUAGE PolyKinds, MultiParamTypeClasses, GADTs, ScopedTypeVariables,
             TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

module Super where

import Data.Proxy
import GHC.Prim

class (a ~ b) => C a b
data SameKind :: k -> k -> * where
  SK :: SameKind a b

bar :: forall (a :: *) (b :: *). C a b => Proxy a -> Proxy b -> ()
bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)
Note: See TracTickets for help on using tickets.