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.