Sorry I wasn't clear. I'm not an expert on the topic but it seems to me that there are two orthogonal concerns:

1) How does the checker retrieve COMPLETE sets.

Currently it seems to "attach" them to data type constructors (e.g. Maybe). If instead it retrieved them by matching types (e.g. "Maybe a", "a") we could write:

{-# COMPLETE LL #-}

From an implementation point of view, it seems to me that finding complete sets would become similar to finding (flexible, overlapping) class instances. Pseudo-code:

class Complete a where
  conlikes :: [ConLike]
instance Complete (Maybe a) where
  conlikes = [Nothing @a, Just @a]
instance Complete (Maybe a) where
  conlikes = [N @a, J @a]
instance Complete a where
  conlikes = [LL @a]
...

2) COMPLETE set depending on the matched type.

It is a thread hijack from me but while we are thinking about refactoring COMPLETE pragmas to support polymorphism, maybe we could support this too. The idea is to build a different set of conlikes depending on the matched type. Pseudo-code:

instance Complete (Variant cs) where
  conlikes = [V @c | c <- cs] -- cs is a type list

(I don't really care about the pragma syntax)

Sorry for the thread hijack!
Regards,
Sylvain

I'm afraid I don't understand what your new syntax means. And, while I know it doesn't work today, what's wrong (in theory) with

{-# COMPLETE LL #-}

No types! (That's a rare thing for me to extol...)

I feel I must be missing something here.

Thanks,

Richard

On Oct 25, 2018, at 12:24 PM, Sylvain Henry <sylvain@haskus.fr> wrote:

> In the case where all the patterns are polymorphic, a user must
> provide a type signature but we accept the definition regardless of
> the type signature they provide. 

Currently we can specify the type *constructor* in a COMPLETE pragma:

pattern J :: a -> Maybe a
pattern J a = Just a

pattern N :: Maybe a
pattern N = Nothing

{-# COMPLETE N, J :: Maybe #-}

Instead if we could specify the type with its free vars, we could refer to them in conlike signatures:

{-# COMPLETE N, [ J :: a -> Maybe a ] :: Maybe a #-}

The COMPLETE pragma for LL could be:

{-# COMPLETE [ LL :: HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a ] :: a #-}

I'm borrowing the list comprehension syntax on purpose because it would allow to define a set of conlikes from a type-list (see my request [1]):

{-# COMPLETE [ V :: (c :< cs) => c -> Variant cs
             | c <- cs
             ] :: Variant cs
  #-}

>    To make things more formal, when the pattern-match checker
> requests a set of constructors for some data type constructor T, the
> checker returns:
>
>    * The original set of data constructors for T
>    * Any COMPLETE sets of type T
>
> Note the use of the phrase *type constructor*. The return type of all
> constructor-like things in a COMPLETE set must all be headed by the
> same type constructor T. Since `LL`'s return type is simply a type
> variable `a`, this simply doesn't work with the design of COMPLETE
> sets.

Could we use a mechanism similar to instance resolution (with FlexibleInstances) for the checker to return matching COMPLETE sets instead?

--Sylvain


[1] https://mail.haskell.org/pipermail/ghc-devs/2018-July/016053.html

_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs