Opened 10 months ago

Closed 4 months ago

## #15076 closed bug (fixed)

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

Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.8.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: | dependent/should_compile/T15076{,b,c} |

Blocked By: | Blocking: | ||

Related Tickets: | #14040, #14880 | Differential Rev(s): | |

Wiki Page: |

### Description (last modified by )

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 (11)

### comment:2 Changed 10 months ago by

Description: | modified (diff) |
---|

### comment:3 Changed 10 months ago by

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 10 months ago by

Related Tickets: | #14040 → #14040, #14880 |
---|

### comment:5 Changed 10 months ago by

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 10 months ago by

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 9 months ago by

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)

### comment:9 Changed 4 months ago by

After commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.), the programs in this ticket no longer panic/throw a Core Lint error. Should we claim victory on this ticket?

### comment:11 Changed 4 months ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Test Case: | → dependent/should_compile/T15076{,b,c} |

Victory!

**Note:**See TracTickets for help on using tickets.

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

`-ddump-tc-trace`

that:Here,

`a_aZo`

is not bound by any implication.