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