Re: Type inference of singular matches on GADTs

29 Mar 2021

      On Sun, Mar 28, 2021 at 11:00:56PM -0400, Carter Schonwald wrote:
...
On Sun, Mar 28, 2021 at 10:19 PM Richard Eisenberg  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.

Re: Type inference of singular matches on GADTs

Viktor Dukhovni