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-applicati... (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-dane@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