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
<sgraf1...@gmail.com <mailto:sgraf1...@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-d...@dukhovni.org <mailto:ietf-d...@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
