GHC panic on pattern synonym

changed weight to 5

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 ***

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 ($).

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

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.

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

mentioned in commit e2998d72

mentioned in commit 307d1dfe

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

Trac metadata

Trac field	Value
Test case	- → testsuite/tests/patsyn/should_fail/T14552

Yeah this is OK

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

mentioned in issue #14880 (closed)

mentioned in commit 5e45ad10

added PatternSynonyms TypeInType ViewPatterns labels

added Pnormal label

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

GHC panic on pattern synonym

Child items ...

Activity