Re: Type inference of singular matches on GADTs

20 Mar 2021


      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)