Type inference of singular matches on GADTs

[Sebastian Graf]

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>:

> 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/20210322/d11b8ef8/attachment.html>