Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,860
    • Issues 4,860
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 454
    • Merge requests 454
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16892
Closed
Open
Created Jul 01, 2019 by Oleg Grenrus@phadejDeveloper

Allow to specify full type for COMPLETE pragmas

Summary

I'd like to be able to write

{-# COMPLETE NSI0                   :: NS Identity '[x0] #-}
{-# COMPLETE NSI0, NSI1             :: NS Identity '[x0, x1] #-}
{-# COMPLETE NSI0, NSI1, NSI2       :: NS Identity '[x0, x1, x2] #-}
{-# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #-}

Motivation

{-# LANGUAGE GADTs, DataKinds, TypeOperators, PatternSynonyms, EmptyCase #-}
{-# OPTIONS_GHC -Wall #-}

import Data.Functor.Identity (Identity (..))

data NS f xs where
    Z :: f x     -> NS f (x ': xs)
    S :: NS f xs -> NS f (x ': xs)

-- ugly

ex01 :: NS Identity '[Int, Char, Bool] -> String
ex01 (Z (Identity i))         = show i
ex01 (S (Z (Identity c)))     = show c
ex01 (S (S (Z (Identity b)))) = show b
ex01 (S (S (S x)))            = case x of {}

-- let's define patterns

pattern NSI0 :: x0 -> NS Identity (x0 ': xs)
pattern NSI0 x = Z (Identity x)

pattern NSI1 :: x1 -> NS Identity (x0 ': x1 ': xs)
pattern NSI1 x = S (Z (Identity x))

pattern NSI2 :: x2 -> NS Identity (x0 ': x1 ': x2 ': xs)
pattern NSI2 x = S (S (Z (Identity x)))

-- ex02 looks nice, but warns
--
-- In an equation for ‘ex02’: Patterns not matched: _

ex02 :: NS Identity '[Int, Char, Bool] -> String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b

-- we can make warning go away with:
{-# COMPLETE NSI0, NSI1, NSI2 #-}

-- but then ex03
-- warns with: Patterns not matched: _
ex03 :: NS Identity '[Int, Char] -> String
ex03 (NSI0 i) = show i
ex03 (NSI1 c) = show c

-- and ex04 is accepted without a warning
ex04 :: NS Identity '[Int, Char, Bool, ()] -> String
ex04 (NSI0 i) = show i
ex04 (NSI1 c) = show c
ex04 (NSI2 b) = show b
-- note missing 4th clause

--
-- I'd like to write {-# COMPLETE NSI0, NSI1, NSI2 :: NS Identity '[x0, x1, x2] #-}
--
-- but that is not accepted

Proposal

Based on a Disambiguating between multiple COMPLETE pragmas section, GHC already does "something" do pick from various matching lists. I propose to add

  • COMPLETE type annotation is at least as polymorphic as pattern scrutinee type,

"at least as polymorphic as"

lhs ≼ rhs

rhs is at least as polymorphic as lhs. ≼ is reflexive.

-- see example 2
forall a. a -> a   ≼  Bool -> Bool

-- see example 1
NS Identity '[x0]  ⊀  NS Identity '[]              
NS Identity '[x0]  ≼  NS Identity '[x0]            
NS Identity '[x0]  ⊀  NS Identity '[x0, x1]        
                      
NS Identity '[x0]  ⊀  NS Identity xs               
NS Identity '[x0]  ⊀  NS Identity (x0 ': xs)       
NS Identity '[x0]  ⊀  NS Identity (x0 ': x1 ': xs) 

-- ^^^ COMPLETE       ^^^ scrutinee type         
--     annotation

Unambiguous

Currently documentation says

The result type must also be unambiguous. Usually this can be inferred but when all the pattern synonyms in a group are polymorphic in the constructor the user must provide a type signature.

I think for my needs requring the type annotation to start with a concrete TyCon is ok. I cannot think how

{-# COMPLETE Pat1, Pat2 :: f ... #-}

could even make sense.

The downside is that we'll need to change

- {-# COMPLETE T :: [] #-}
+ {-# COMPLETE T :: [a] #-}

Example 1

given there are

{-# COMPLETE NSI0                   :: NS Identity '[x0] #-}
{-# COMPLETE NSI0, NSI1             :: NS Identity '[x0, x1] #-}
{-# COMPLETE NSI0, NSI1, NSI2       :: NS Identity '[x0, x1, x2] #-}
{-# COMPLETE NSI0, NSI1, NSI2, NSI3 :: NS Identity '[x0, x1, x2, x3] #-}

pragmas, and we are considering

ex02 :: NS Identity '[Int, Char, Bool] -> String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b

then only 3rd pragma "match".

Variation

There is (almost) a problematic case:

ex03 :: NS Identity (Int ': Char ': Bool ': xs) -> String
ex02 (NSI0 i) = show i
ex02 (NSI1 c) = show c
ex02 (NSI2 b) = show b

then the the scrutinee type is NS Identity (Int ': Char ': Bool': xs), and none of the specified above COMPLETE pragmas match/apply.

If one adds another pattern synonym, with new COMPLETE pragma:

pattern Rest2 :: NS f xs -> NS f (x0 ': x1 ': xs)
pattern Rest2 x = S (S x)

{-# COMPLETE NSI0, NSI1, Rest2 :: NS Identity (x0 ': x1 ': xs) #-}

In this case, all the above scenarios same warnings will be produced. But if we write

ex03 :: NS Identity (Int ': Char ': xs) -> String
ex03 (NSI0 i)  = show i
ex03 (NSI1 c)  = show c
ex03 (Rest2 _) = "rest"

it will be accepted without warnings as well. Note:

NS Identity (x0 ': x1 ': xs) ≼ NS Identity '[Int, Char, Bool]

from ex02. But as there is a COMPLETE pragma set which doesn't produce any warnings, none warnings are reported.

Example 2

The below snipped fors already today

pattern Endo :: (a -> a) -> (a -> a)
pattern Endo f = f

{-# COMPLETE Endo :: (->) #-}

double :: (a -> a) -> (a -> a)
double (Endo f) = Endo (f . f)

The pragma should be changed to

{-# COMPLETE Endo :: a -> a #-} -- as in pattern type decl.

if we however specify only

{-# COMPLETE Endo :: Int -> Int #-}

then

Int -> Int ⊀ forall a. a -> a

and incomplete match warning would be printed.

Edited Jul 01, 2019 by Oleg Grenrus
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking