haskellconstraint-kindstype-synonyms

Haskell: interaction between ConstraintKinds, and TypeSynonymInstances


I'm getting an unexpected error when trying to compile a small Haskell file with GHC 8.6.1 when using ConstraintKinds and TypeSynonymInstances.

I'd like to make a class that takes a class as a parameter, and I'd like to use an alias when writing an instance. Here's the code:

{-# LANGUAGE ConstraintKinds, KindSignatures, TypeSynonymInstances #-}

module TypeAlias where

import Data.Kind

class Foo a
class Bar a

class Baz (c :: * -> Constraint)

instance Baz Foo -- compiles
instance Baz Bar -- compiles

type FooBar a = (Foo a, Bar a) -- compiles

instance Baz FooBar -- fails!
-- TypeAlias.hs:17:10-19: error:
--     • The type synonym ‘FooBar’ should have 1 argument, but has been given none
--     • In the instance declaration for ‘Baz FooBar’
--    |
-- 17 | instance Baz FooBar
--    |          ^^^^^^^^^^

The error is surprising because, as far as I can tell, FooBar has the expected kind, namely * -> Constraint, but the compiler says it should be fed an argument.

Is it even possible to use a constraint alias in an instance declaration as I am trying here? If so, how do I make sense of the seemingly contradictory error message?

(I know I can simply declare FooBar as a class instead of an alias, but I really don't want to because I'd also want an instance and at that point I'd have to pull in UndecidableInstances.)


Solution

  • Turns out, Ed Kmett answered my question a year ago. I can't do it with type aliases, but using UndecidableInstances should be benign for this particular situation:

    https://www.reddit.com/r/haskell/comments/5zjwym/when_is_undecidableinstances_okay_to_use/

    Here's how Kmett might suggest fixing the above example:

    {-# LANGUAGE ConstraintKinds, FlexibleInstances,
                 KindSignatures, UndecidableInstances #-}
    
    module NotTypeAlias where
    
    import Data.Kind
    
    class Foo a
    class Bar a
    
    class Baz (c :: * -> Constraint)
    
    instance Baz Foo -- compiles
    instance Baz Bar -- compiles
    
    class (Foo a, Bar a) => FooBar a
    instance (Foo a, Bar a) => FooBar a -- compiles
    
    instance Baz FooBar -- compiles
    

    Kmett argues that if the instance of FooBar we provide is the sole instance ever in scope, then the type checker won't fall into an infinite loop from our use of UndecidableInstances. I'm satisfied to take him at his word.