GHC panic with defer-typed-holes

Does this still happen in HEAD?

import qualified GHC.Generics as GHC
import Generics.SOP
import Generics.SOP.TH
import Data.Proxy

gminbound' :: (Generic a, Code a ~ (xs:xss), All2 Bounded (Code a)) => a
gminbound' = minBound
  & I
  & hcpure (Proxy @Bounded)
  & apInjs_POP
  & head
  & to

Fails but doesn't crash with

$ ghci -ignore-dot-ghci -XTypeApplications -XTypeOperators -XDataKinds -XGADTs -XFlexibleContexts /tmp/tX96.hs 
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/tX96.hs, interpreted )

/tmp/tX96.hs:8:3: error:
    Variable not in scope: (&) :: t4 -> (a0 -> I a0) -> t3

/tmp/tX96.hs:9:3: error:
    Variable not in scope: (&) :: t3 -> t5 -> t2

/tmp/tX96.hs:10:3: error:
    Variable not in scope:
      (&) :: t2 -> (POP f1 xss0 -> [SOP f1 xss0]) -> t1

/tmp/tX96.hs:11:3: error:
    Variable not in scope: (&) :: t1 -> ([a1] -> a1) -> t0

/tmp/tX96.hs:12:3: error:
    Variable not in scope: (&) :: t0 -> (Rep a2 -> a2) -> a
Failed, modules loaded: none.
Prelude> 

but crashes with -fdefer-typed-holes

$ ghci -ignore-dot-ghci -fdefer-typed-holes -XTypeApplications -XTypeOperators -XDataKinds -XGADTs -XFlexibleContexts /tmp/tX96.hs 
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/tX96.hs, interpreted )

/tmp/tX96.hs:8:3: warning: [-Wtyped-holes]
    Variable not in scope: (&) :: t4 -> (a0 -> I a0) -> t3

/tmp/tX96.hs:9:3: warning: [-Wtyped-holes]
    Variable not in scope: (&) :: t3 -> t5 -> t2

/tmp/tX96.hs:10:3: warning: [-Wtyped-holes]
    Variable not in scope:
      (&) :: t2 -> (POP f1 xss0 -> [SOP f1 xss0]) -> t1

/tmp/tX96.hs:11:3: warning: [-Wtyped-holes]
    Variable not in scope: (&) :: t1 -> ([a1] -> a1) -> t0

/tmp/tX96.hs:12:3: warning: [-Wtyped-holes]
    Variable not in scope: (&) :: t0 -> (Rep a2 -> a2) -> a
ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.1 for x86_64-unknown-linux):
        opt_univ fell into a hole {aabX}

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

> 

---

More minimal example, still requires generics-sop:

import Generics.SOP

a = minBound
  & hcpure (Proxy @Bounded)

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

Simplified version without any dependencies (generics-sop):

import Data.Proxy

hcpure :: proxy c -> (forall a. c a => f a) -> h f xs
hcpure _ _ = undefined

a = minBound
  & hcpure (Proxy @Bounded)

This is a good use case for #393 (closed), because of the rank-2 type we need to supply two wildcard arguments.

mentioned in issue #12598

Hmm. In HEAD (and therefore I think 8.0 but I'm not certain) an out-of-scope variable is an error, so we get

T12589.hs:11:14: error: Variable not in scope: (&) :: t0 -> t1 -> t

regardless of -fefer-typed-holes. If I change it to be

a = _foo minBound (hcpure (Proxy @Bounded))

using a named wildcard, with -defer-typed-holes in HEAD I get

s:12:5: warning: [-Wtyped-holes]
    * Found hole: _foo :: t0 -> t1 -> t
      Where: `t0' is an ambiguous type variable
             `t1' is an ambiguous type variable
             `t' is a rigid type variable bound by
               the inferred type of a :: t at T12589.hs:12:1-43
      Or perhaps `_foo' is mis-spelled, or not in scope
    * In the expression: _foo
      In the expression: _foo minBound (hcpure (Proxy @Bounded))
      In an equation for `a': a = _foo minBound (hcpure (Proxy @Bounded))
    * Relevant bindings include a :: t (bound at T12589.hs:12:1)

T12589.hs:12:20: warning: [-Wdeferred-type-errors]
    * Cannot instantiate unification variable `t1'
      with a type involving foralls:
        (forall a. Bounded a => f0 a) -> h0 f0 xs0
        GHC doesn't yet support impredicative polymorphism
    * In the second argument of `_foo', namely
        `(hcpure (Proxy @Bounded))'
      In the expression: _foo minBound (hcpure (Proxy @Bounded))
      In an equation for `a': a = _foo minBound (hcpure (Proxy @Bounded))

which is what I'd expect.

I have not investigated the "falling ito a hole" error becuase it just doesn't happen in HEAD.

So could someone test with 8.0.1? If it's ok there then let's just add a regression test and declare it fixed.

This program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

import Data.Proxy

hcpure :: proxy c -> (forall a. c a => f a) -> h f xs
hcpure _ _ = undefined

a = minBound
  & hcpure (Proxy @Bounded)

produces that GHC panic with GHC 8.0.1, but not with GHC 8.0.2 or HEAD.

It appears that af21e388 was the commit that fixed this.

mentioned in commit 042c5930

Since this test will also work in GHC 8.0.2, the above commit can be safely merged.

Trac metadata

Trac field	Value
Test case	- → typecheck/should_fail/T12589

added 1 deleted label

closed

changed milestone to %8.0.2

Test merged to ghc-8.0 as 9467dfa8.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Pnormal label