Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project
    • Project
    • Details
    • Activity
    • Releases
    • Cycle Analytics
    • Insights
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
    • Locked Files
  • Issues 3,625
    • Issues 3,625
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 198
    • Merge Requests 198
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Security & Compliance
    • Security & Compliance
    • Dependency List
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #9953

Closed
Open
Opened Jan 02, 2015 by Simon Peyton Jones@simonpj
  • Report abuse
  • New issue
Report abuse New issue

Pattern synonyms don't work with GADTs

Consider this variant of test T8968-1:

{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where

data X :: * -> * where
  Y :: a -> X (Maybe a)

pattern C :: a -> X (Maybe a)
pattern C x = Y x

foo :: X t -> t
foo (C x) = Just x
  • If we had (Y x) instead of (C x) in the LHS of foo, then this is an ordinary GADT program and typechecks fine.
  • If we omit the pattern signature, it typechecks fine, and :info C says
pattern C :: t ~ Maybe a => a -> X t 	-- Defined in ‘ShouldCompile’
  • But as written, it fails with
Foo.hs:11:6:
    Couldn't match type ‘t’ with ‘Maybe a0’
      ‘t’ is a rigid type variable bound by
          the type signature for: foo :: X t -> t at Foo.hs:10:8
    Expected type: X t
      Actual type: X (Maybe a0)
    Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
    In the pattern: C x
    In an equation for ‘foo’: foo (C x) = Just x

Moreover, :info C says

pattern C :: a -> X (Maybe a) 	-- Defined at Foo.hs:8:9

Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit.

The exact thing happens for DataCons. It's handled via the dcEqSpec field. Essentially PatSyn should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in TcTyClsDecls.rejigConRes (perhaps needs a better name).

This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.

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

Related issues

  • Discussion
  • Designs
Assignee
Assign to
7.10.1
Milestone
7.10.1
Assign milestone
Time tracking
None
Due date
None
4
Labels
bug P::normal Trac import typechecker
Assign labels
  • View project labels
Reference: ghc/ghc#9953