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.