Opened 2 months ago

Last modified 5 days ago

#14135 new bug

PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull)

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.4.1
Component: Compiler Version: 8.3
Keywords: PatternSynonyms Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3981
Wiki Page:

Description

This code works in GHC 8.2:

{-# LANGUAGE PatternSynonyms #-}
module Bug where

data Foo a = Foo1 a | Foo2 a

pattern MyFoo2 :: Int -> Foo Int
pattern MyFoo2 i = Foo2 i

{-# COMPLETE Foo1, MyFoo2 #-}

f :: Foo a -> a
f (Foo1 x) = x

But it throws a compile-time exception on GHC HEAD:

$ ghc3/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170815 for x86_64-unknown-linux):
        expectJust mkOneConFull
CallStack (from HasCallStack):
  error, called at compiler/utils/Maybes.hs:53:27 in ghc:Maybes
  expectJust, called at compiler/deSugar/Check.hs:1128:37 in ghc:Check

Change History (12)

comment:1 Changed 2 months ago by RyanGlScott

Version: 8.2.18.3

comment:2 Changed 2 months ago by RyanGlScott

Cc: simonpj added

Commit 6b77914cd37b697354611bcd87897885c1e5b4a6 (Fix instantiation of pattern synonyms) is responsible for this regression.

comment:3 Changed 5 weeks ago by carlostome

Owner: set to carlostome

comment:4 Changed 5 weeks ago by carlostome

I've found that this error is caused by the order of the arguments to tcMatchTy in the following code.

mkOneConFull x con = do
  let res_ty  = idType x
      (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
        = conLikeFullSig con
      tc_args = tyConAppArgs res_ty
      subst1  = case con of
                  RealDataCon {} -> zipTvSubst univ_tvs tc_args
                  PatSynCon {}   -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
  ...

Adding some debugging information I noticed that the call that makes tcMatchTy return Nothing and therefore trigger the error it is done with the following arguments (as outputed with -dppr-debug):

  con_res_ty = main:T14135.Foo{tc r9} ghc-prim:GHC.Types.Int{(w) tc 3u}
  res_ty     = main:T14135.Foo{tc r9} (a{tv aWz} [tv] :: *) 

As far as I understand the problem stands because tcMatchTy expects the first argument to be a kind of template type that will get instantiated to match the second argument. However, it is clear that there is no substitution s such that s(Int) = a.

If we change the call to tcMatchTy res_ty con_res_ty then the example program compiles fine but when trying to validate, ghc is not able to build anymore Data.Typeable.Internal because it triggers the exactly same error.

I have found that by substituting tcMatchTy by tcUnifyTy we solve the full problem, however, I don't know if tcMatchTy should be prefered over tcUnify or not (if it makes a semantic difference).

Any insight on this?

comment:5 Changed 5 weeks ago by carlostome

Differential Rev(s): Phab:D3981

comment:6 Changed 5 weeks ago by simonpj

OK I can see what is happening here. The trouble is with the COMPLETE pragma (again!).

Suppose we'd written

f :: Foo a -> a
f (Foo1 x)   = x
f (MyFoo2 y) = y

This definition is rejected as ill-typed:

T14135.hs:13:4: error:
    * Couldn't match type `a' with `Int'
      `a' is a rigid type variable bound by
        the type signature for:
          f :: forall a. Foo a -> a
        at T14135.hs:11:1-15
      Expected type: Foo a
        Actual type: Foo Int

Reason: the pattern synonym MyFoo2 demands that its scrutinee has type Foo Int. This is unlike a GADT, whose data constructors can have a return type Foo Int but which can match a scrutinee of type Foo a. It's a conscious design choice, described in the user manual (I hope). See Note [Pattern synonym result type] in PatSyn.

Now, the overlap checker, when looking for missing patterns, effectively adds that extra equation. But the extra equation is ill-typed which crashes the overlap checker. (So yes, I think the tcMatchTy is fine; it's relying on the scrutinee having the right type.)

So what are we to make of {-# COMPLETE Foo1, MyFoo2 #-}? The simplest thing to do is to insist that all the constructors in a COMPLETE pragma match the same type of scrutinee, where

  • A constructor K declared thus
    data T a b where
      K :: ....
    
    matches a scrutinee of type T a b (NB: NOT the return type in K's signature which for a GADT might be T Int Bool)
  • A constructor K declared in a data instance
    data instance T ty1 ty2 where
      K :: ....
    
    matches a scrutinee of type T ty1 ty2. (NB: again, not the return type in K's signature which may an instance of K ty1 ty2)
  • A constructor K declared in a pattern synonym
    pattern K :: .... -> T ty1 ty2
    
    matches a scrutinee of type T ty1 ty2.

If we did this check when dealing with the COMPLETE pragma, I think that's solve this crash.

comment:7 Changed 5 weeks ago by RyanGlScott

This type-of-scrutinee check is interesting, but it would come at a cost. Currently, it is quite possible to use Foo1 and MyFoo2 together, in this function:

g :: Foo Int -> Int
g (Foo1 x)   = x
g (MyFoo2 y) = y

But if we adopted your proposed type-of-scrutinee validity check, then we'd no longer be able to write a COMPLETE program that covers this use case, since {-# COMPLETE Foo1, MyFoo2 #-} wouldn't typecheck.

comment:8 Changed 5 weeks ago by simonpj

OK, well, another alternative (triggered by #14253 comment:9), filter the candidate COMPLETE sets, to choose only those all of whose constructors match the type of the scrutinee. So in the example in comment:7 we'd use the COMPLETE pragma, but in the example in the Description we would ignore it.

comment:9 Changed 5 weeks ago by RyanGlScott

That sounds like a great suggestion to me!

This might even scratch an itch I discovered in https://ghc.haskell.org/trac/ghc/ticket/14059#comment:2. There, I lamented that fact that I wanted to write a COMPLETE set for a group of conlikes whose types are headed by Sing. The problem was that each conlike wasn't of type, say, Sing (a :: k), but rather the more specific type Sing (a :: Bool). But with the proposal laid out in comment:8, I don't believe this would be an issue, since we could simply filter out anything in a COMPLETE set that wasn't of type Sing (a :: Bool). Nice.

comment:10 Changed 2 weeks ago by simonpj

Anyone want to try doing this? Currently we just crash which is bad.

comment:11 Changed 2 weeks ago by RyanGlScott

Status: newpatch

carlostome appears to be working on this in Phab:D3981. However, he appears to be stuck, so any advice would be appreciated over at Phab:D3981.

comment:12 Changed 5 days ago by carlostome

Owner: carlostome deleted
Status: patchnew

I'm still stuck on this, and right now I don't have that much time to work on it. I'll drop it for someone else to work on it.

Note: See TracTickets for help on using tickets.