Opened 12 months ago

Closed 10 months ago

Last modified 3 weeks ago

#14552 closed bug (fixed)

GHC panic on pattern synonym

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: PatternSynonyms, TypeInType, ViewPatterns Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: testsuite/tests/patsyn/should_fail/T14552
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}

import Data.Kind

data family Sing a

type a --> b = (a, b) -> Type

type family (@@) (f::a --> b) (x::a) :: b

data Proxy a = Proxy

newtype Limit' :: (k --> Type) -> Type where
  Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f

data Exp :: [Type] -> Type -> Type where
  TLam' :: Proxy f
        -> (forall aa. Proxy aa -> Exp xs (f @@ aa))
        -> Exp xs (Limit' f)

pattern FOO f <- TLam' Proxy (($ Proxy) -> f)

--->

$ ghci -ignore-dot-ghci 119-bug.hs 
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 119-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20171122 for x86_64-unknown-linux):
	ASSERT failed!
  in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC}
  tenv [a1MC :-> r_a1MC]
  cenv []
  tys [k_a1Mj[ssk:3]]
  cos []
  needInScope [a1Mj :-> k_a1Mj[ssk:3]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
        substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
        substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
        substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
        substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst

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

> 

Change History (12)

comment:1 Changed 11 months ago by RyanGlScott

If you don't have a build with ASSERTions enabled, then you can also trigger a Core Lint with this program as well:

$ /opt/ghc/8.2.2/bin/ghci Bug.hs -dcore-lint
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the type ‘forall (r :: TYPE rep) (a :: [*]) b (aa :: k).
                 Exp a b
                 -> (forall k1 (f :: k1 --> *).
                     (b :: *) ~# (Limit' f :: *) =>
                     Exp a (f @@ aa) -> r)
                 -> (Void# -> r)
                 -> r’
    @ k_a1K2[ssk:3] is out of scope
*** Offending Program ***
$mFOO
  :: forall (r :: TYPE rep) (a :: [*]) b (aa :: k).
     Exp a b
     -> (forall k1 (f :: k1 --> *).
         (b :: *) ~# (Limit' f :: *) =>
         Exp a (f @@ aa) -> r)
     -> (Void# -> r)
     -> r
[LclIdX]
$mFOO
  = \ (@ (rep_a1Kn :: RuntimeRep))
      (@ (r_a1Ko :: TYPE rep_a1Kn))
      (@ (a_a1K0 :: [*]))
      (@ b_a1K1)
      (@ (aa_a1Kc :: k_a1K2[ssk:3]))
      (scrut_a1Kq :: Exp a_a1K0 b_a1K1)
      (cont_a1Kr
         :: forall k1 (f :: k1 --> *).
            (b_a1K1 :: *) ~# (Limit' f :: *) =>
            Exp a_a1K0 (f @@ aa_a1Kc) -> r_a1Ko)
      _ [Occ=Dead] ->
      break<0>(scrut_a1Kq,cont_a1Kr)
      case scrut_a1Kq of
      { TLam' @ k_a1K2 @ f_a1K3 cobox_a1K4 ds_d1Lm ds_d1Ln ->
      case ds_d1Lm of { Proxy ->
      cont_a1Kr
        @ k_a1K2
        @ f_a1K3
        @~ (cobox_a1K4 :: (b_a1K1 :: *) ~# (Limit' f_a1K3 :: *))
        ((\ (ds_d1Lp [OS=OneShot]
               :: Proxy aa_a1Kc -> Exp a_a1K0 (f_a1K3 @@ aa_a1Kc)) ->
            $ @ 'LiftedRep
              @ (Proxy aa_a1Kc)
              @ (Exp a_a1K0 (f_a1K3 @@ aa_a1Kc))
              ds_d1Lp
              (Proxy @ k_a1K2 @ aa_a1Kc))
           (ds_d1Ln @ aa_a1Kc))
      }
      }

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

$krep_a1Lc [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lc
  = KindRepTyConApp $tc[] (: @ KindRep krep$* ([] @ KindRep))

$krep_a1Lb [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lb = KindRepFun $krep_a1Lc krep$*Arr*

$krep_a1Lg [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lg = $WKindRepVar (I# 0#)

$krep_a1Lh [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lh = KindRepFun $krep_a1Lg krep$*

$krep_a1Lf [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lf
  = KindRepTyConApp
      $tc(,) (: @ KindRep $krep_a1Lg (: @ KindRep krep$* ([] @ KindRep)))

$krep_a1Le [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Le = KindRepFun $krep_a1Lf krep$*

$krep_a1Ld [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Ld = KindRepFun $krep_a1Le krep$*

$krep_a1Lj [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Lj = $WKindRepVar (I# 1#)

$tcSing :: TyCon
[LclIdX]
$tcSing
  = TyCon
      18130532723012807500##
      591365583239837277##
      $trModule
      (TrNameS "Sing"#)
      0#
      krep$*Arr*

$tcProxy :: TyCon
[LclIdX]
$tcProxy
  = TyCon
      637564349063008466##
      16772998216715059205##
      $trModule
      (TrNameS "Proxy"#)
      1#
      $krep_a1Lh

$krep_a1Li [InlPrag=[~]] :: KindRep
[LclId]
$krep_a1Li
  = KindRepTyConApp
      $tcProxy
      (: @ KindRep $krep_a1Lg (: @ KindRep $krep_a1Lj ([] @ KindRep)))

$tc'Proxy :: TyCon
[LclIdX]
$tc'Proxy
  = TyCon
      10313009608267148799##
      11340514327723585599##
      $trModule
      (TrNameS "'Proxy"#)
      2#
      $krep_a1Li

$tcLimit' :: TyCon
[LclIdX]
$tcLimit'
  = TyCon
      15980210257158400910##
      15895439795101193324##
      $trModule
      (TrNameS "Limit'"#)
      1#
      $krep_a1Ld

$tcExp :: TyCon
[LclIdX]
$tcExp
  = TyCon
      14856342479466933336##
      11891426334869696372##
      $trModule
      (TrNameS "Exp"#)
      0#
      $krep_a1Lb

*** End of Offense ***

comment:2 Changed 11 months ago by goldfire

Simon asked me to take a look at this pattern synonym, as there are deeper issues here.

Here is a much simpler scenario with similar issues:

data T where
  T :: (forall a. Int -> a -> a) -> T

pattern PT x <- T (($ 3) -> x)

What type should PT have? Here are two possibilities: (renaming for clarity, but both have the same definition)

pattern PT1 :: forall a. (a -> a) -> T
pattern PT2 :: (forall a. a -> a) -> T

These synonyms correspond to the following two matchers:

matcher1 :: forall r a. T -> ((a -> a) -> r) -> r
matcher1 (T f) k = k (f 3)

matcher2 :: forall r. T -> ((forall a. a -> a) -> r) -> r
matcher2 (T f) k = k (f 3)

Both type-check. The second is more general than the first, even though the first is what GHC infers for the definition if given the chance. So, which matcher should we generate for PT?

However, I've just played a trick on you. Notice that I inlined the use of ($) in my matchers. Interestingly, matcher2 does not type check without this inlining:

matcher2 (T (($ 3) -> x)) k = k x   -- does not type-check

This fails because it contains an unsaturated use of ($), and unsaturated uses of ($) do not get the pseudo-impredicative magic that saturated uses of ($) get. So, really, matcher1 is the only possibility. (Indeed, GHC infers a pattern type of forall a. (a -> a) -> T for PT.)

In the original program, the question above (where to generalize) isn't properly formed. That's because the equivalent of the a here (called aa in the example) has an existentially-bound kind, so it can't possibly scope over the whole matcher type. (In other words, it can't be like matcher1.) As I've already argued, it also can't be like matcher2 (because ($) isn't impredicative in this scenario). So, it must be like matcher3:

matcher3 :: forall r. T -> ((Any -> Any) -> r) -> r
matcher3 (T (($ 3) -> x)) k = k x

This is a bit silly, but it's the best we can do if we can't generalize over a. In the original program, this is really

matcher :: Exp xs t -> (forall k (f :: k --> Type). Exp xs (f @@ Any) -> r) -> r
matcher (TLam (Proxy :: Proxy this_f) (($ (Proxy @Any)) -> z)) k = k @_ @this_f z

Probably not what the user wanted, but I don't see how we can do better without an impredicative unsaturated ($).

comment:3 Changed 11 months ago by Iceland_jack

This is crazy. Does it make a difference if ($ 3) got expanded (\f -> f 3)?

comment:4 Changed 11 months ago by simonpj

Let's make it even simpler. Use Richard's data type T, and consider

{-# LANGUAGE ViewPatterns, RankNTypes, GADTs  #-}
module Foo where

data T where
  T :: (forall a. Int -> a -> a) -> T

g1 (T f) = (f 3 'c', f 3 True)

g2 (T f) = let h = f 3
           in (h 'c', h True)

g3 (T (id -> f)) = (f 3 'c', f 3 True)

g4 (T ((\f -> f 3) -> h)) = (h 'c', h True)

Here we get

  • g1 typechecks because f is bound to a polymorphic function.
  • g2 does not typecheck, because the binding of h is not generalised (we have MonoLocalBinds when GADTs is on). So h is monomorphic.
  • g3 does not typecheck for the same reason. It's akin to g2 with h = id f; it desugars to something like
    g3 (T ff) = let f = id ff
                in (f 3 'c', f 3 True)
    
  • g4 does not typecheck for the same reason. It desugars to something like
    g4 (T ff) = let h = (\f -> f 3) ff
                in (h 'c', h True)
    

So I don't think this has anything to do with the impredicativity magic for ($). It's just that binding a polymorphic variable in a pattern is a very delicate business. One could imagine generalising those extra let-bindings in the desugarings of g3 and g4, but would be hard to do reliably -- that is why we have MonoLocalBinds.

comment:5 Changed 11 months ago by simonpj

PS

Interestingly, matcher2 does not type check without this inlining:

It does for me!

matcher3 (T (($ 3) -> x)) k = k x

typechecks just fine with inferred type

matcher3 :: forall a t. T -> ((a -> a) -> t) -> t

comment:6 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In e2998d72/ghc:

Stop double-stacktrace in ASSERT failures

We were getting the stack trace printed twice in assertion
failures (e.g. see the Description of Trac #14552).

This fixes it, by deleting code.

(c.f. Trac #14635 which reports the same bug in documentation).

comment:7 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In 307d1df/ghc:

Fix deep, dark corner of pattern synonyms

Trac #14552 showed a very obscure case where we can't infer a
good pattern-synonym type.

The error message is horrible, but at least we no longer crash
and burn.

comment:8 Changed 11 months ago by simonpj

Test Case: testsuite/tests/patsyn/should_fail/T14552

OK the main fix here is comment:7. I'm not terribly happy with the error message, but it's better than a crash. Iceland Jack: ok?

comment:9 Changed 11 months ago by RyanGlScott

Status: newinfoneeded

comment:10 Changed 11 months ago by Iceland_jack

Yeah this is OK

comment:11 Changed 10 months ago by simonpj

Resolution: fixed
Status: infoneededclosed

comment:12 Changed 3 weeks ago by Richard Eisenberg <rae@…>

In 5e45ad10/ghc:

Finish fix for #14880.

The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.

Fixing this required reworking candidateQTyVarsOfType, the function
that extracts free variables as candidates for quantification.
One consequence is that we now must be more careful when quantifying:
any skolems around must be quantified manually, and quantifyTyVars
will now only quantify over metavariables. This makes good sense,
as skolems are generally user-written and are listed in the AST.

As a bonus, we now have more control over the ordering of such
skolems.

Along the way, this commit fixes #15711 and refines the fix
to #14552 (by accepted a program that was previously rejected,
as we can now accept that program by zapping variables to Any).

This commit also does a fair amount of rejiggering kind inference
of datatypes. Notably, we now can skip the generalization step
in kcTyClGroup for types with CUSKs, because we get the
kind right the first time. This commit also thus fixes #15743 and
 #15592, which both concern datatype kind generalisation.
(#15591 is also very relevant.) For this aspect of the commit, see
Note [Required, Specified, and Inferred in types] in TcTyClsDecls.

Test cases: dependent/should_fail/T14880{,-2},
            dependent/should_fail/T15743[cd]
            dependent/should_compile/T15743{,e}
            ghci/scripts/T15743b
            polykinds/T15592
            dependent/should_fail/T15591[bc]
            ghci/scripts/T15591
Note: See TracTickets for help on using tickets.