Type inference of singular matches on GADTs
Viktor Dukhovni
ietf-dane at dukhovni.org
Mon Mar 29 06:31:50 UTC 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 <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.
More information about the ghc-devs
mailing list