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>: > 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>: > >> 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 >> >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
