Type inference of singular matches on GADTs

[Sebastian Graf]

Hi Alexis,

The following works and will have inferred type `Int`:

> bar = foo (\(HNil :: HList '[]) -> 42)

I'd really like it if we could write

> bar2 = foo (\(HNil @'[]) -> 42)

though, even if you write out the constructor type with explicit
constraints and forall's.
E.g. by using a -XTypeApplications here, I specify the universal type var
of the type constructor `HList`. I think that is a semantics that is in
line with Type Variables in Patterns, Section 4
<https://dl.acm.org/doi/10.1145/3242744.3242753>: The only way to satisfy
the `as ~ '[]` constraint in the HNil pattern is to refine the type of the
pattern match to `HList '[]`. Consequently, the local `Blah '[]` can be
discharged and bar2 will have inferred `Int`.

But that's simply not implemented at the moment, I think. I recall there's
some work that has to happen before. The corresponding proposal seems to be
https://ghc-proposals.readthedocs.io/en/latest/proposals/0126-type-applications-in-patterns.html
(or https://github.com/ghc-proposals/ghc-proposals/pull/238? I'm confused)
and your example should probably be added there as motivation.

If `'[]` is never mentioned anywhere in the pattern like in the original
example, I wouldn't expect it to type-check (or at least emit a
pattern-match warning): First off, the type is ambiguous. It's a similar
situation as in
https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell.
If it was accepted and got type `Blah as => Int`, then you'd get a
pattern-match warning, because depending on how `as` is instantiated, your
pattern-match is incomplete. E.g., `bar3 @[Int]` would crash.

Complete example code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

module Lib where

data HList as where
  HNil  :: forall as. (as ~ '[]) => HList as
  HCons :: forall as a as'. (as ~ (a ': as')) => a -> HList as' -> HList as

class Blah as where
  blah :: HList as

instance Blah '[] where
  blah = HNil

foo :: Blah as => (HList as -> Int) -> Int
foo f = f blah

bar = foo (\(HNil :: HList '[]) -> 42) -- compiles
bar2 = foo (\(HNil @'[]) -> 42) -- errors

Cheers,
Sebastian

Am Sa., 20. März 2021 um 13:57 Uhr schrieb Viktor Dukhovni <
ietf-dane at dukhovni.org>:

> On Sat, Mar 20, 2021 at 08:13:18AM -0400, Viktor Dukhovni wrote:
>
> > As soon as I try add more complex contraints, I appear to need an
> > explicit type signature for HNil, and then the code again compiles:
>
> But aliasing the promoted constructors via pattern synonyms, and using
> those instead, appears to resolve the ambiguity.
>
> --
>     Viktor.
>
> {-# LANGUAGE
>     DataKinds
>   , GADTs
>   , PatternSynonyms
>   , PolyKinds
>   , ScopedTypeVariables
>   , TypeFamilies
>   , TypeOperators
>   #-}
>
> import GHC.Types
>
> infixr 1 `HC`
>
> data HList as where
>   HNil  :: HList '[]
>   HCons :: a -> HList as -> HList (a ': as)
>
> pattern HN :: HList '[];
> pattern HN = HNil
> pattern HC :: a -> HList as -> HList (a ': as)
> pattern HC a as = HCons a as
>
> class Nogo a where
>
> type family   Blah (as :: [Type]) :: Constraint
> type instance Blah '[]        = ()
> type instance Blah (_ ': '[]) = ()
> type instance Blah (_ ': _ ': '[]) = ()
> type instance Blah (_ ': _ ': _ ': _) = (Nogo ())
>
> foo :: (Blah as) => (HList as -> Int) -> Int
> foo _ = 42
>
> bar :: Int
> bar = foo (\ HN -> 1)
>
> baz :: Int
> baz = foo (\ (True `HC` HN) -> 2)
>
> pattern One :: Int
> pattern One = 1
> bam :: Int
> bam = foo (\ (True `HC` One `HC` HN) -> 2)
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210320/ffd1b6a6/attachment.html>