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