<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>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:</p>
<blockquote>
<pre>baz :: Int -> String -> Widget
baz = ....
bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b)
</pre>
</blockquote>
<p>I don’t want to have to annotate the types of <tt>a</tt> and <tt>b</tt>
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.</p>
<p>Really what I’m complaining about here is type inference of GADT
patterns. For comparison, suppose I had these definitions:</p>
<blockquote>
<pre>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)
</pre>
</blockquote>
<p>This compiles without any issues. The pattern <tt>(a, b)</tt> is
inferred to have type <tt>(t1, t2)</tt>, where both <tt>t1</tt>
and <tt>t2</tt> are metavariables. These are unified to
particular types in the body, and everything is fine.</p>
<p>But type inference for GADT patterns works differently. In fact,
even this simple definition fails to compile:</p>
<blockquote>
<pre>bar = \(a `HCons` HNil) -> not a
</pre>
</blockquote>
<p>GHC rejects it with the following error:</p>
<blockquote>
<pre>error:
• Could not deduce: a ~ Bool
from the context: as ~ (a : as1)
</pre>
</blockquote>
<p>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 <i>could</i> 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 <i>wanted</i>
to write a non-exhaustive function on an arbitrary <tt>HList</tt>.</p>
<p>Of course, I think that’s somewhat silly. If there’s a single
principal type that makes my function well-typed <i>and
exhaustive</i>, I’d really like GHC to pick it.</p>
<p>Alexis<br>
</p>
<div class="moz-cite-prefix">On 3/22/21 1:28 PM, Sebastian Graf
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAAS+=P8bU9pL7foO6LA_hahB2WQoYCZfwU=55gKG8FD+vo0xPQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>Cale made me aware of the fact that the "Type applications
in patterns" proposal had already been implemented.</div>
<div>See <a
href="https://gitlab.haskell.org/ghc/ghc/-/issues/19577"
moz-do-not-send="true">https://gitlab.haskell.org/ghc/ghc/-/issues/19577</a>
where I adapt Alexis' use case into a test case that I'd like
to see compiling.<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Am Sa., 20. März 2021 um
15:45 Uhr schrieb Sebastian Graf <<a
href="mailto:sgraf1337@gmail.com" moz-do-not-send="true">sgraf1337@gmail.com</a>>:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr">
<div>Hi Alexis,</div>
<div><br>
</div>
<div>The following works and will have inferred type `Int`:</div>
<div><br>
</div>
<div>> bar = foo (\(HNil :: HList '[]) -> 42) <br>
</div>
<div><br>
</div>
<div>I'd really like it if we could write</div>
<div><br>
</div>
<div>> bar2 = foo (\(HNil @'[]) -> 42)
</div>
<div><br>
</div>
<div>though, even if you write out the constructor type with
explicit constraints and forall's.</div>
<div>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 <a
href="https://dl.acm.org/doi/10.1145/3242744.3242753"
target="_blank" moz-do-not-send="true">Type Variables in
Patterns, Section 4</a>: 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`.<br>
</div>
<div><br>
</div>
<div>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 <a
href="https://ghc-proposals.readthedocs.io/en/latest/proposals/0126-type-applications-in-patterns.html"
target="_blank" moz-do-not-send="true">https://ghc-proposals.readthedocs.io/en/latest/proposals/0126-type-applications-in-patterns.html</a>
(or <a
href="https://github.com/ghc-proposals/ghc-proposals/pull/238"
target="_blank" moz-do-not-send="true">https://github.com/ghc-proposals/ghc-proposals/pull/238</a>?
I'm confused) and your example should probably be added
there as motivation.</div>
<div><br>
</div>
<div>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 <a
href="https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell"
target="_blank" moz-do-not-send="true">https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell</a>.
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.</div>
<div><br>
</div>
<div>Complete example code:</div>
<div><br>
</div>
<div>{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE LambdaCase #-}<br>
{-# LANGUAGE TypeApplications #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
{-# LANGUAGE RankNTypes #-}<br>
<br>
module Lib where<br>
<br>
data HList as where<br>
HNil :: forall as. (as ~ '[]) => HList as<br>
HCons :: forall as a as'. (as ~ (a ': as')) => a
-> HList as' -> HList as<br>
<br>
class Blah as where<br>
blah :: HList as<br>
<br>
instance Blah '[] where<br>
blah = HNil<br>
<br>
foo :: Blah as => (HList as -> Int) -> Int<br>
foo f = f blah<br>
</div>
<br>
<div>bar = foo (\(HNil :: HList '[]) -> 42) -- compiles</div>
<div>bar2 = foo (\(HNil @'[]) -> 42) -- errors</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Sebastian<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Am Sa., 20. März 2021 um
13:57 Uhr schrieb Viktor Dukhovni <<a
href="mailto:ietf-dane@dukhovni.org" target="_blank"
moz-do-not-send="true">ietf-dane@dukhovni.org</a>>:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">On Sat, Mar 20, 2021 at
08:13:18AM -0400, Viktor Dukhovni wrote:<br>
<br>
> As soon as I try add more complex contraints, I
appear to need an<br>
> explicit type signature for HNil, and then the code
again compiles:<br>
<br>
But aliasing the promoted constructors via pattern
synonyms, and using<br>
those instead, appears to resolve the ambiguity.<br>
<br>
-- <br>
Viktor.<br>
<br>
{-# LANGUAGE<br>
DataKinds<br>
, GADTs<br>
, PatternSynonyms<br>
, PolyKinds<br>
, ScopedTypeVariables<br>
, TypeFamilies<br>
, TypeOperators<br>
#-}<br>
<br>
import GHC.Types<br>
<br>
infixr 1 `HC`<br>
<br>
data HList as where<br>
HNil :: HList '[]<br>
HCons :: a -> HList as -> HList (a ': as)<br>
<br>
pattern HN :: HList '[];<br>
pattern HN = HNil<br>
pattern HC :: a -> HList as -> HList (a ': as)<br>
pattern HC a as = HCons a as<br>
<br>
class Nogo a where<br>
<br>
type family Blah (as :: [Type]) :: Constraint<br>
type instance Blah '[] = ()<br>
type instance Blah (_ ': '[]) = ()<br>
type instance Blah (_ ': _ ': '[]) = ()<br>
type instance Blah (_ ': _ ': _ ': _) = (Nogo ())<br>
<br>
foo :: (Blah as) => (HList as -> Int) -> Int <br>
foo _ = 42<br>
<br>
bar :: Int<br>
bar = foo (\ HN -> 1)<br>
<br>
baz :: Int<br>
baz = foo (\ (True `HC` HN) -> 2)<br>
<br>
pattern One :: Int<br>
pattern One = 1<br>
bam :: Int<br>
bam = foo (\ (True `HC` One `HC` HN) -> 2)</blockquote>
</div>
</blockquote>
</div>
</blockquote>
</body>
</html>