Skip to content

GHC doesn't see () as a Constraint in type family

See also #9547

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, MultiParamTypeClasses, TypeFamilies #-}

import GHC.Exts

class NotFound

type family 
  F b where
  F 'False = (NotFound :: Constraint)
  F 'True  = (() :: Constraint)

works fine. Removing all constraints and final line it works without any annotations and infers the type of F :: Bool -> Constraint:

type family
  F b where
  F 'False = NotFound

GHC seems determined that () :: Type unless explicitly told otherwise, I would like to be able to write:

type family 
  F b where
  F 'False = NotFound
  F 'True  = ()

Edit by @sgraf812: The latter compiles at least since 9.0. What does not compile is if you switch the clauses:

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, MultiParamTypeClasses, TypeFamilies #-}

module T11621 where

import GHC.Exts

class NotFound

type family
  F b where
  F 'True  = ()
  F 'False = NotFound

See #11621 (comment 164668) for explanation.

Edited by Sebastian Graf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information