#15692 closed bug (fixed)

GHC panic from pattern synonyms + deferred type errors

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.2
Component: Compiler Version: 8.6.1
Keywords: PatternSynonyms Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: patsyn/should_fail/T15692
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}

{-# Options_GHC -dcore-lint -fdefer-type-errors #-}

import Data.Kind

data Ctx :: Type -> Type where
 E     :: Ctx(Type)
 (:&:) :: a -> Ctx(as) -> Ctx(a -> as)

data ApplyT (k::Type) :: k ->  Ctx(k) -> Type where
 AO :: a -> ApplyT(Type) a E
 AS :: ApplyT(ks)      (f a) ctx
    -> ApplyT(k -> ks) f     (a:&:ctx)

pattern ASSO = AS (AS (AO False))
$ ghci -ignore-dot-ghci 463.hs
hs/463.hs:16:27: warning: [-Wdeferred-type-errors]
    • Couldn't match type ‘a a1 a2’ with ‘Bool’
      Expected type: a3
        Actual type: Bool
    • In the pattern: False
      In the pattern: AO False
      In the pattern: AS (AO False)
   |
16 | pattern ASSO = AS (AS (AO False))
   |                           ^^^^^
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20180828 for x86_64-unknown-linux):
	urk! lookup local fingerprint
  $mASSO
  [iESflb :-> ($trModule, 1ca40dc83a9c879effdb760462cc9a2d),
   iESgKD :-> ($tc'E, 79f67a27a14dc1bb6eecb39e4b061e2c),
   iESgKF :-> ($tc':&:, 24793c0c1652ffcf92e04f47d38fa075),
   iESgKH :-> ($tcCtx, a3f9358cbfe161bf59e75500d70ce0ae),
   iESgKI :-> ($tc'AO, 72111d1891cb082e989c20a2191a8b4b),
   iESgKK :-> ($tc'AS, ff019c04c400d5fbdd46ff8a816d4913),
   iESgKM :-> ($tcApplyT, cbfe28374b4115925c7213e6330ab115)]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/iface/MkIface.hs:524:37 in ghc:MkIface

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

> 

Change History (8)

comment:1 Changed 12 months ago by RyanGlScott

Keywords: TypeInType removed

Here's a version which doesn't require any TypeInType voodoo:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where

data F x where
  FS :: F (f a) -> F a

pattern FS' = FS False
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:9:18: warning: [-Wdeferred-type-errors]
    • Couldn't match expected type ‘F (f x)’ with actual type ‘Bool’
    • In the pattern: False
      In the pattern: FS False
      In the declaration for pattern synonym ‘FS'’
  |
9 | pattern FS' = FS False
  |                  ^^^^^
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.1 for x86_64-unknown-linux):
        urk! lookup local fingerprint
  $mFS'
  [iESfI6 :-> ($trModule, 550028d00664444fecdab255e6368e70),
   iESgIq :-> ($tc'FS, a6b7c6b435bb17f938e26b19c786b9e3),
   iESgIs :-> ($tcF, 59ff366e0583120727f8be6ecf210589)]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/iface/MkIface.hs:524:37 in ghc:MkIface

This is a regression from GHC 8.4.3:

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

Bug.hs:9:18: warning: [-Wdeferred-type-errors]
    • Couldn't match expected type ‘F (f x)’ with actual type ‘Bool’
    • In the pattern: False
      In the pattern: FS False
      In the declaration for pattern synonym ‘FS'’
  |
9 | pattern FS' = FS False
  |                  ^^^^^

Bug.hs:9:18: warning: [-Wdeferred-type-errors]
    • Couldn't match expected type ‘F (f0 x)’ with actual type ‘Bool’
    • In the first argument of ‘FS’, namely ‘False’
      In the expression: FS False
      In an equation for ‘FS'’: FS' = FS False
    • Relevant bindings include $bFS' :: F x (bound at Bug.hs:9:9)
  |
9 | pattern FS' = FS False
  |                  ^^^^^

comment:2 Changed 12 months ago by RyanGlScott

Cc: simonpj added

Somewhat ironically, commit 149d7912eb84a24861b021c13d2ee61b44de5856 (Fix error recovery for pattern synonyms) introduced this.

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

In 9ebfa03/ghc:

Fail fast on pattern synonyms

We were recovering too eagerly from errors in pattern-synonym
type inference, leading to a cascade of confusing follow up errors
(Trac #15685, #15692).

The underlying issue is that a pattern synonym should have a closed,
fixed type, with no unification variables in it.  But it wasn't!

Fixing this made me change the interface to simplifyInfer slightly.
Instead of /emitting/ a residual implication constraint, it
now /returns/ it, so that the caller can decide what to do.

comment:4 Changed 12 months ago by simonpj

Status: newmerge
Test Case: patsyn/should_fail/T15692

Thanks.

This fix could probably be merged. It modifies a bit more code than I'd usually like in a patch-release, but I'm pretty confident. And it validates of course.

comment:5 Changed 12 months ago by RyanGlScott

Milestone: 8.6.18.6.2

comment:6 Changed 12 months ago by Iceland_jack

Is this the same issue?

{-# Language DataKinds, PatternSynonyms, KindSignatures, GADTs #-}

{-# Options_GHC -fdefer-type-errors #-}

import Data.Kind

data N = O | S N

data Fin :: N -> Type where
  FinO :: Fin (S n)

data Exists :: (Type -> Type) -> Type where
  Exists :: f xx -> Exists f  

pattern O' = Exists FinO
$ ghci -ignore-dot-ghci hs/486.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/486.hs, interpreted )

hs/486.hs:15:21: warning: [-Wdeferred-type-errors]
    • Couldn't match kind ‘*’ with ‘N’
      When matching types
        a :: * -> *
        Fin :: N -> *
      Expected type: a xx
        Actual type: Fin a0
    • In the pattern: FinO
      In the pattern: Exists FinO
      In the declaration for pattern synonym ‘O'’
   |
15 | pattern O' = Exists FinO
   |                     ^^^^
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20180828 for x86_64-unknown-linux):
	urk! lookup local fingerprint
  $mO'
  [iESflb :-> ($trModule, 1ca40dc83a9c879effdb760462cc9a2d),
   iESgex :-> ($tc'O, 111d9d0cf0cb57db9c77a4d216344e54),
   iESgKA :-> ($tc'S, 2d7f65aefd4d8c7deac332c17204e2c9),
   iESgKC :-> ($tcN, 04f8b57a4955bc680fd71fe4cee31a00),
   iESgKD :-> ($tc'FinO, a20e4215870bd6fb39afb23de637e84a),
   iESgKF :-> ($tcFin, 8a38d4451422cc87d0cc0459132dad73),
   iESgKG :-> ($tc'Exists, 365c3f6bd1b8c9580d1ae883b83c2c68),
   iESgKI :-> ($tcExists, 11a84f66f5d99fe1d3547c0ad0f538ae)]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/iface/MkIface.hs:524:37 in ghc:MkIface

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

> 

comment:7 in reply to:  6 Changed 12 months ago by RyanGlScott

Replying to Iceland_jack:

Is this the same issue?

Yes.

comment:8 Changed 11 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.