Opened 14 months ago

Closed 13 months ago

Last modified 13 months ago

#11524 closed bug (fixed)

Something is amiss with quantification in pattern synonym type signatures

Reported by: bgamari Owned by:
Priority: high Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: PatternSynonyms Cc: mpickering, niteria
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1879, Phab:D1896
Wiki Page:

Description

Consider this program,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}

module Test where

data AType (a :: k) where
    AMaybe :: AType Maybe
    AInt :: AType Int
    AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). AType a -> AType b -> AType (a b)

pattern PApp :: () => (fun ~ a b) => AType a -> AType b -> AType fun
--pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1).
--            () => (fun ~ a b) => AType a -> AType b -> AType fun
pattern PApp fun arg <- AApp fun arg

I would have thought that the two type signatures would be equivalent. However, when I use the quantified signature GHC complains with,

hi.hs:14:34: error:
    • Expected kind ‘AType a’, but ‘fun’ has kind ‘AType a1’
    • In the declaration for pattern synonym ‘PApp’
    • Relevant bindings include
        arg :: AType b1 (bound at hi.hs:14:34)
        fun :: AType a1 (bound at hi.hs:14:30)

Moreover, if I use the un-quantified signature and ask GHCi for the full type signature, it gives me the precisely the quantified type that it rejected previously,

λ> :info PApp
pattern PApp :: forall k (fun :: k) k1 (a :: k1
                                             -> k) (b :: k1). () => fun ~ a b => AType a
                                                                                 -> AType b
                                                                                 -> AType fun
  	-- Defined at hi.hs:14:1

Very odd.

Change History (13)

comment:1 Changed 14 months ago by goldfire

It's a bug in the pretty-printer. Here is the correct version with explicit quantification:

pattern PApp :: forall k2 (fun :: k2). ()
             => forall k1 (a :: k1 -> k2) (b :: k1). (fun ~ a b) 
             => AType a -> AType b -> AType fun

Note that k2 and fun are universal, while k1, a, and b are existential. And indeed this signature is accepted.

Two problems remain:

  1. That error message is unhelpful. I imagine we can do better.
  1. The pretty-printer should put the existentials in the right spot.
Last edited 14 months ago by goldfire (previous) (diff)

comment:2 Changed 14 months ago by bgamari

Cc: niteria added

It's a bug in the pretty-printer.

Actually, I'm not entirely sure that this is the whole story.

After pulling I'm now seeing with both the correctly-quantified and the unquantified signature,

$ inplace/bin/ghc-stage1 hi.hs
[1 of 1] Compiling Main             ( hi.hs, hi.o )
ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 8.1.20160124 for x86_64-unknown-linux):
	ASSERT failed!
  file compiler/types/TyCoRep.hs line 1919
  in_scope InScope {k_aB4 k_aJd a_aJe b_aJf}
  tenv [auE :-> a_aJe[tau:5], auF :-> b_aJf[tau:5],
        aB3 :-> k_aJd[tau:5]]
  cenv []
  tys [fun_auD[sk] ~ a_auE[sk] b_auF[sk]]
  cos []
  needInScope [auD :-> fun_auD[sk], aB4 :-> k_aB4[tau:1]]

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

Presumably this is niteria's in-scope set checks in action.

Last edited 14 months ago by bgamari (previous) (diff)

comment:3 Changed 14 months ago by niteria

Better trace with ghc-stage2:

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160128 for x86_64-unknown-linux):
        ASSERT failed!
  CallStack (from ImplicitParams):
  assertPprPanic, called at compiler/types/TyCoRep.hs:1932:51 in ghc:TyCoRep
  checkValidSubst, called at compiler/types/TyCoRep.hs:1981:17 in ghc:TyCoRep
  substTys, called at compiler/types/TyCoRep.hs:2002:14 in ghc:TyCoRep
  substTheta, called at compiler/typecheck/TcPatSyn.hs:254:57 in ghc:TcPatSyn
  in_scope InScope {k_aB3 k_aB8 a_aB9 b_aBa}
  tenv [auD :-> a_aB9[tau:5], auE :-> b_aBa[tau:5],
        aB2 :-> k_aB8[tau:5]]
  cenv []
  tys [fun_auC[sk] ~ a_auD[sk] b_auE[sk]]
  cos []
  needInScope [auC :-> fun_auC[sk], aB3 :-> k_aB3[tau:1]]

comment:4 Changed 14 months ago by niteria

Differential Rev(s): Phab:D1879
Status: newpatch

comment:5 Changed 14 months ago by goldfire

NB: niteria's (quite necessary) patch does not fix the main issue reported up top. When that patch is merged, we still can't close this ticket.

comment:6 Changed 14 months ago by mpickering

Keywords: PatternSynonyms added

comment:7 Changed 14 months ago by Bartosz Nitka <niteria@…>

In 07ed2413/ghc:

Use a correct substitution in tcCheckPatSynDecl

The `substTheta` call didn't have the free variables of the
`prov_theta` in the `in_scope` set. It should be enough to add
`univ_tvs`, as all the `ex_tvs` are already in the domain of
the substitution.

Test Plan: added a testcase

Reviewers: simonpj, bgamari, goldfire, austin

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1879

GHC Trac Issues: #11524

comment:8 Changed 14 months ago by niteria

Status: patchnew

comment:9 Changed 14 months ago by simonpj

Could someone fix the pretty-printer (comment:1)?

comment:10 in reply to:  9 Changed 13 months ago by rdragon

Differential Rev(s): Phab:D1879Phab:D1879, Phab:D1896

See Phab:D1896 for a fix of the pretty-printer.

comment:11 Changed 13 months ago by Ben Gamari <ben@…>

In 3801262e/ghc:

Fix printing of an `IfacePatSyn`

Now the existentially quantified type variables are printed
at the correct location when printing a pattern synonym type
from an `IfacePatSyn`. The function `pprIfaceContextMaybe`
has been removed as it is no longer needed.

Fixes #11524.

Reviewers: austin, goldfire, thomie, bgamari, mpickering

Reviewed By: bgamari

Differential Revision: https://phabricator.haskell.org/D1958

GHC Trac Issues: #11524

comment:12 Changed 13 months ago by bgamari

Last edited 13 months ago by bgamari (previous) (diff)

comment:13 Changed 13 months ago by bgamari

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