Opened 3 years ago

Closed 3 years ago

#8966 closed bug (fixed)

Pattern synonyms and kind-polymorphism

Reported by: kosmikus Owned by: simonpj
Priority: normal Milestone: 7.8.3
Component: Compiler (Type checker) Version: 7.8.1-rc2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: patsyn/T8966
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


There's a strange interaction between pattern synonyms, GADTs, kind polymorphism and data kinds.

The following module fails to compile with ghc-7.8.1-rc2, but I think it should:

{-# LANGUAGE PolyKinds, KindSignatures, PatternSynonyms, DataKinds, GADTs #-}

data NQ :: [k] -> * where
  D :: NQ '[a]

pattern Q = D

I get the following error:

    Could not deduce (a ~ a0)
    from the context (t ~ '[a])
      bound by the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
      at KindPat.hs:6:9
      ‘a’ is a rigid type variable bound by
          the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
          at KindPat.hs:6:13
    Expected type: NQ t
      Actual type: NQ '[a0]
    In the expression: D
    In an equation for ‘$WQ’: ($WQ) = D

Change History (5)

comment:1 Changed 3 years ago by simonpj

Owner: set to simonpj

Thanks. A zonking step is missing. Patch coming.

comment:2 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 4dc9f9869bfc82fdb8bd61864859007873ebcc27/ghc:

Zonk the existential type variables in tcPatSynDecl

This was just an omission, which showed up as Trac #8966

comment:3 Changed 3 years ago by simonpj

Status: newmerge
Test Case: patsyn/T8966

Good catch, thank you.

Please merge to 7.8 branch in due course.


comment:4 Changed 3 years ago by thoughtpolice

Milestone: 7.8.3

comment:5 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to 7.8.

Note: See TracTickets for help on using tickets.