Type inference of singular matches on GADTs

[Viktor Dukhovni]

On Sun, Mar 28, 2021 at 11:00:56PM -0400, Carter Schonwald wrote:

> On Sun, Mar 28, 2021 at 10:19 PM Richard Eisenberg <rae at richarde.dev> wrote:
>
> > I think this is the key part of Alexis's plea: that the type checker take
> > into account exhaustivity in choosing how to proceed.
> >
> > Another way to think about this:
> >
> > f1 :: HList '[] -> ()
> > f1 HNil = ()
> >
> > f2 :: HList as -> ()
> > f2 HNil = ()
> >
> > Both f1 and f2 are well typed definitions. In any usage site where both
> > are well-typed, they will behave the same. Yet f1 is exhaustive while f2 is
> > not. ...
>
> I like how you've boiled down this discussion, it makes it much clearer to
> me at least :)

+1.  Very much distills it for me too.  Thanks!

FWIW, I've since boiled down the pattern-synonym example to the below,
where I find the choices of ":^" and ":$" to be pleasantly mnemonic,
though "HSolo" is perhaps a bit too distracting...

    {-# language DataKinds, FlexibleInstances, FlexibleContexts, GADTs
               , PatternSynonyms, TypeOperators #-}
    {-# OPTIONS_GHC -Wno-type-defaults #-}
    import Data.Reflection
    import Data.Proxy

    default (Int)

    data HList as where
      HNil_  :: HList '[]
      HCons_ :: a -> HList as -> HList (a ': as)
    infixr 5 `HCons_`

    pattern HNil :: HList '[];
    pattern HNil  = HNil_

    pattern HSolo :: a -> HList '[a]
    pattern HSolo a = a :^ HNil

    pattern (:^) :: a -> HList as -> HList (a ': as)
    pattern (:^) a as = HCons_ a as
    infixr 5 :^

    pattern (:$) :: a -> b -> HList '[a,b]
    pattern (:$) a b = a :^ HSolo b
    infixr 5 :$

    hApp :: Reifies s (HList as) => (HList as -> r) -> Proxy s -> r
    hApp f = f . reflect

    main :: IO ()
    main = do
        print $ reify HNil          $ hApp (\ HNil     -> 42)
        print $ reify (HSolo    42) $ hApp (\ (HSolo a) -> a)
        print $ reify (28 :$ "0xe") $ hApp (\ (a :$ b) -> a + read b)

-- 
    Viktor.