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