<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">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">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">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">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">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">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">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)<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>
</blockquote></div>