Type inference of singular matches on GADTs

[Alexis King]

I appreciate your point Sebastian, but I think in this particular case, 
type applications in patterns are still not enough to satisfy me. I 
provided the empty argument list example because it was simple, but I’d 
also like this to typecheck:

    baz :: Int -> String -> Widget
    baz = ....

    bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b)

I don’t want to have to annotate the types of a and b because they’re 
both eminently inferrable. I’d like to get type inference properties 
comparable to an ordinary two-argument lambda expression, since that’s 
how I’m trying to use this, after all.

Really what I’m complaining about here is type inference of GADT 
patterns. For comparison, suppose I had these definitions:

    class Blah a where
       foo :: (a -> Widget) -> Whatsit

    instance Blah (Int, String) where
       foo = ....

    baz :: Int -> String -> Widget
    baz = ....

    bar = foo (\(a, b) -> baz a b)

This compiles without any issues. The pattern (a, b) is inferred to have 
type (t1, t2), where both t1 and t2 are metavariables. These are unified 
to particular types in the body, and everything is fine.

But type inference for GADT patterns works differently. In fact, even 
this simple definition fails to compile:

    bar = \(a `HCons` HNil) -> not a

GHC rejects it with the following error:

    error:
         • Could not deduce: a ~ Bool
           from the context: as ~ (a : as1)

This seems to arise from GHC’s strong reluctance to pick any particular 
type for a match on a GADT constructor. One way to explain this is as a 
sort of “open world assumption” as it applies to case expressions: we 
always /could/ add more cases, and if we did, specializing the type 
based on the existing cases might be premature. Furthermore, 
non-exhaustive pattern-matching is not a type error in Haskell, only a 
warning, so perhaps we /wanted/ to write a non-exhaustive function on an 
arbitrary HList.

Of course, I think that’s somewhat silly. If there’s a single principal 
type that makes my function well-typed /and exhaustive/, I’d really like 
GHC to pick it.

Alexis

On 3/22/21 1:28 PM, Sebastian Graf wrote:
> Cale made me aware of the fact that the "Type applications in 
> patterns" proposal had already been implemented.
> See https://gitlab.haskell.org/ghc/ghc/-/issues/19577 where I adapt 
> Alexis' use case into a test case that I'd like to see compiling.
>
> Am Sa., 20. März 2021 um 15:45 Uhr schrieb Sebastian Graf 
> <sgraf1337 at gmail.com <mailto:sgraf1337 at gmail.com>>:
>
>     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 <mailto: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)
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210326/53b91921/attachment.html>