Opened 3 months ago

Closed 3 months ago

#15629 closed bug (fixed)

"No skolem info" panic (GHC 8.6 only)

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

Description

The following program:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Proxy
import GHC.Generics

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

data family Sing :: forall k. k -> Type
newtype instance Sing (f :: k1 ~> k2) =
  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t -> Sing (Apply f t)) -> Sing f
singFun1 f = SLambda f

data From1Sym0 :: forall k (f :: k -> Type) (a :: k). f a ~> Rep1 f a
data To1Sym0   :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a

type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
  (f :. g) x = Apply f (Apply g x)

data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x

(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
        Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)

(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
           Sing f -> Sing g -> Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)

f :: forall (m :: Type -> Type) x. Proxy (m x) -> ()
f _ = ()
  where
    sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
    sFrom1Fun = undefined

    sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
    sTo1Fun = undefined

    sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
    sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun

Panics on GHC 8.6:

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:50:39: error:
    • Expected kind ‘m z ~> Rep1 m ab1’,
        but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
    • In the first argument of ‘(.@#@$$$)’, namely
        ‘(From1Sym0 :: m z ~> Rep1 m z)’
      In the first argument of ‘Sing’, namely
        ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                              ~> Rep1 m ab)’
      In the type signature:
        sFrom1To1Fun :: forall ab.
                        Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                                                  ~> Rep1 m ab)
   |
50 |     sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180823 for x86_64-unknown-linux):
        No skolem info:
  [ab_a1UW[sk:1]]
  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

But merely errors on GHC 8.4.3:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs   
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:50:39: error:
    • Expected kind ‘m z ~> Rep1 m ab2’,
        but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
    • In the first argument of ‘(.@#@$$$)’, namely
        ‘(From1Sym0 :: m z ~> Rep1 m z)’
      In the first argument of ‘Sing’, namely
        ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                              ~> Rep1 m ab)’
      In the type signature:
        sFrom1To1Fun :: forall ab.
                        Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                                                  ~> Rep1 m ab)
   |
50 |     sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:51:20: error:
    • Couldn't match type ‘ab1’ with ‘z1’
        because type variable ‘z1’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
        at Bug.hs:50:5-112
      Expected type: Sing From1Sym0
        Actual type: Sing From1Sym0
    • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
      In the expression: sFrom1Fun %.$$$ sTo1Fun
      In an equation for ‘sFrom1To1Fun’:
          sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
    • Relevant bindings include
        sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
          (bound at Bug.hs:51:5)
   |
51 |     sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
   |                    ^^^^^^^^^

Bug.hs:51:36: error:
    • Couldn't match type ‘ab’ with ‘z1’
        because type variable ‘z1’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
        at Bug.hs:50:5-112
      Expected type: Sing To1Sym0
        Actual type: Sing To1Sym0
    • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
      In the expression: sFrom1Fun %.$$$ sTo1Fun
      In an equation for ‘sFrom1To1Fun’:
          sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
    • Relevant bindings include
        sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
          (bound at Bug.hs:51:5)
   |
51 |     sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
   |                                    ^^^^^^^

Change History (10)

comment:1 Changed 3 months ago by RyanGlScott

Blimey, it looks like this has been fixed on GHC HEAD:

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

Bug.hs:50:39: error:
    • Expected kind ‘m z ~> Rep1 m ab’,
        but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
    • In the first argument of ‘(.@#@$$$)’, namely
        ‘(From1Sym0 :: m z ~> Rep1 m z)’
      In the first argument of ‘Sing’, namely
        ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                              ~> Rep1 m ab)’
      In the type signature:
        sFrom1To1Fun :: forall ab.
                        Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
                                                                                  ~> Rep1 m ab)
   |
50 |     sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:51:20: error:
    • Couldn't match type ‘z’ with ‘ab’
      ‘z’ is a rigid type variable bound by
        the type signature for:
          sFrom1To1Fun :: forall z1 ab1. Sing (From1Sym0 .@#@$$$ To1Sym0)
        at Bug.hs:50:5-112
      ‘ab’ is a rigid type variable bound by
        the type signature for:
          sFrom1To1Fun :: forall z1 ab1. Sing (From1Sym0 .@#@$$$ To1Sym0)
        at Bug.hs:50:5-112
      Expected type: Sing (From1Sym0 .@#@$$$ To1Sym0)
        Actual type: Sing (From1Sym0 .@#@$$$ To1Sym0)
    • In the expression: sFrom1Fun %.$$$ sTo1Fun
      In an equation for ‘sFrom1To1Fun’:
          sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
      In an equation for ‘f’:
          f _
            = ()
            where
                sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
                sFrom1Fun = undefined
                sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
                sTo1Fun = undefined
                ....
    • Relevant bindings include
        sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
          (bound at Bug.hs:51:5)
   |
51 |     sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
   |                    ^^^^^^^^^^^^^^^^^^^^^^^

I'm dying to know what fixed this...

comment:2 Changed 3 months ago by simonpj

Interesting! I'm sure you are bisecting as we speak.

It'd be good to add a regression test regardless. Thanks!

comment:3 Changed 3 months ago by RyanGlScott

Found it. It's commit 042df603cbb5a77ec13ccfec2ce7bad2bb940aae:

From 042df603cbb5a77ec13ccfec2ce7bad2bb940aae Mon Sep 17 00:00:00 2001
From: Richard Eisenberg <rae@cs.brynmawr.edu>
Date: Thu, 5 Jul 2018 14:21:43 -0400
Subject: [PATCH] Unwrap casts before checking vars in eager unifier

Previously, checking whether (tv |> co) ~ (tv |> co) got deferred,
because we looked for vars before stripping casts. (The left type
would get stripped, and then tv ~ (tv |> co) would scare the occurs-
checker.)

This opportunity for improvement presented itself in other work.
This is just an optimization. Some programs can now report more
errors simultaneously.

Pretty impressive for "just an optimization" :)

And yes, we should absolutely add a regression test for this, since I couldn't find another program of this caliber in the test suite currently.

comment:4 Changed 3 months ago by simonpj

Oh my, hang on. Everything should work if the eager unifier does NOTHING. Indeed, I'd love to have a flag -fno-eager-unifier which switches off the eager unifier in order to stress the constraint solver.

It'd b easy: in TcUnify.uType, test the flag and call uType_defer immediately if -fno-eager-unifier is set.

I bet this shows up lots of bugs, so I partly fear to suggest it :-). For this one, does the No skolem come back?

Last edited 3 months ago by simonpj (previous) (diff)

comment:5 Changed 3 months ago by RyanGlScott

In a quick hack, I added a -fno-eager-unifier flag:

  • compiler/main/DynFlags.hs

    diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
    index 9f0ba57..a2f269d 100644
    a b data GeneralFlag 
    557557   | Opt_OptimalApplicativeDo
    558558   | Opt_VersionMacros
    559559   | Opt_WholeArchiveHsLibs
     560   | Opt_NoEagerUnifier
    560561   -- copy all libs into a single folder prior to linking binaries
    561562   -- this should elivate the excessive command line limit restrictions
    562563   -- on windows, by only requiring a single -L argument instead of
    dynamic_flags_deps = [ 
    30173018  , make_ord_flag defGhcFlag "dhex-word-literals"
    30183019        (NoArg (setGeneralFlag Opt_HexWordLiterals))
    30193020
     3021
    30203022  , make_ord_flag defGhcFlag "ghcversion-file"      (hasArg addGhcVersionFile)
    30213023  , make_ord_flag defGhcFlag "main-is"              (SepArg setMainIs)
    30223024  , make_ord_flag defGhcFlag "haddock"              (NoArg (setGeneralFlag Opt_Haddock))
    fFlagsDeps = [ 
    40034005  flagSpec "show-warning-groups"              Opt_ShowWarnGroups,
    40044006  flagSpec "hide-source-paths"                Opt_HideSourcePaths,
    40054007  flagSpec "show-loaded-modules"              Opt_ShowLoadedModules,
    4006   flagSpec "whole-archive-hs-libs"            Opt_WholeArchiveHsLibs
     4008  flagSpec "whole-archive-hs-libs"            Opt_WholeArchiveHsLibs,
     4009  flagSpec "no-eager-unifier"                 Opt_NoEagerUnifier
    40074010  ]
    40084011  ++ fHoleFlags
    40094012
  • compiler/typecheck/TcUnify.hs

    diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
    index 045132e..fb937b7 100644
    a b uType_defer t_or_k origin ty1 ty2 
    13481348
    13491349--------------
    13501350uType t_or_k origin orig_ty1 orig_ty2
    1351   = do { tclvl <- getTcLevel
     1351  = do { no_eager <- goptM Opt_NoEagerUnifier
     1352       ; if no_eager
     1353         then uType_defer t_or_k origin orig_ty1 orig_ty2
     1354         else do
     1355       { tclvl <- getTcLevel
    13521356       ; traceTc "u_tys" $ vcat
    13531357              [ text "tclvl" <+> ppr tclvl
    13541358              , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
    uType t_or_k origin orig_ty1 orig_ty2 
    13571361       ; if isReflCo co
    13581362            then traceTc "u_tys yields no coercion" Outputable.empty
    13591363            else traceTc "u_tys yields coercion:" (ppr co)
    1360        ; return co }
     1364       ; return co } }
    13611365  where
    13621366    go :: TcType -> TcType -> TcM CoercionN
    13631367        -- The arguments to 'go' are always semantically identical

However, the panic does not reappear if you compile the original program with -fno-eager-unifier. The only differences I could observe were minor variations in error quality. With -fno-eager-unifier enabled, you don't see any of the "‘z’ is a rigid type variable bound by..." stuff, for instance.

comment:6 Changed 3 months ago by simonpj

OK -- that's good! If the flag stays, it should probably be -feager-unifier (on by default) because we have generic -fnoxxx machinery.

I'm still very suspicious that the Real Bug is not fixed, just somehow hidden by the patch. So I'm a bit reluctant to declare victory and close.

comment:7 Changed 3 months ago by RyanGlScott

For what it's worth, here is a slightly more minimal version of the original program:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug (f) where

import Data.Kind
import Data.Proxy

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

type family F x :: Type -> Type
data F1Sym :: forall x a. x ~> F x a
data F2Sym :: forall x a. F x a ~> x
data Comp :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)

sg :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
      Proxy f -> Proxy g -> Proxy (Comp f g)
sg _ _ = Proxy

f :: forall (x :: Type). Proxy x -> ()
f _ = ()
  where
    g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
    g = sg Proxy Proxy

comment:8 Changed 3 months ago by simonpj

Well, I devoted a few mins to trying to see what caused the crash in ghc 8.6, but it doesn't look related to the patch you identify in comment:3. Still, since it is working, I'm disinclined to invest more effort in debugging 8.6!

I'll add a regression test and close this.

comment:9 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In 0d4f394/ghc:

Add regression test for Trac #15629

comment:10 Changed 3 months ago by RyanGlScott

Milestone: 8.6.18.8.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T15629
Note: See TracTickets for help on using tickets.