7

How can I constrain to Maybe a where Eq a? It needs to be of kind * -> Constraint

What I tried:

class (a ~ Maybe b, Eq b) => K a where
instance (a ~ Maybe b, Eq b) => K a where

Error:

Not in scope: type variable ‘b’

Example Usage:

data Test c = forall a. (c a) => Test a
r :: Test K -> Maybe Bool
r (Test o) = (==) <$> o <*> o -- I need GHC to infer that o is Maybe Eq

Cases that work:

pp :: Test ((~) String) -> String
pp (Test o) = o ++ "X" -- GHC infers that o is a string

hh :: Test Eq -> Bool
hh (Test o) = o == o -- GHC infers that o is Eq

Generic answer here: Is there a general way to apply constraints to a type application?

Community
  • 1
  • 1
michaelmesser
  • 3,601
  • 2
  • 19
  • 42

2 Answers2

9

The following compiles on my machine. No idea how sensible it is.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
class (Eq (UnMaybe a), a ~ Maybe (UnMaybe a)) => EqMaybe a where
    type UnMaybe a

instance Eq a => EqMaybe (Maybe a) where
    type UnMaybe (Maybe a) = a

data Test c = forall a. c a => Test a
r :: Test EqMaybe -> Maybe Bool
r (Test o) = (==) <$> o <*> o
f :: Test Eq -> Test EqMaybe
f (Test o) = Test (Just o)
Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • Given that there is such a strict constraint `b ~ Maybe a`, it is a bit annoying to have to include both `a` and `b` in the instance head. – Alec Dec 13 '16 at 00:22
  • `fj1 :: Test Eq -> Test (EqMaybe b)` `fj1 (Test o) = Test $ Just o` – michaelmesser Dec 13 '16 at 01:58
  • • Could not deduce (EqMaybe b (Maybe a)) arising from a use of ‘Test’ from the context: Eq a – michaelmesser Dec 13 '16 at 01:58
  • @2426021684 Fixed. – Daniel Wagner Dec 13 '16 at 02:09
  • @DanielWagner Very nice! This is the trick dfeuer keeps using (adding the constraint in both directions to facilitate type inference) - I really need to get the hang of this. – Alec Dec 13 '16 at 02:16
  • Tiny quibble: there's no reason for `UnMaybe` to be an associated type. I think it's clearer as a closed type family: `type family UnMaybe m where UnMaybe (Maybe a) = a`. – dfeuer Dec 13 '16 at 08:41
  • One more quibble: you might as well make the instance head fully polymorphic as well. This will involve less duplication if you use a type synonym for the constraint. – dfeuer Dec 13 '16 at 08:58
  • @dfeuer Regarding the closed type family: unless you are planning on adding a second catch all case and have it report a `TypeError`, isn't the type family better like this? At you can be sure it will never end up stuck... – Alec Dec 13 '16 at 09:25
  • @Alec, it can still be stuck. Nothing stops one from applying it to an arbitrary type. – dfeuer Dec 13 '16 at 13:45
  • @dfeuer Is it possible to generalize this by writing a `((* -> *) -> Constraint) -> (* -> Constraint) -> * -> Constraint` type function?` `(F ((~) Maybe) Eq)` – michaelmesser Dec 14 '16 at 19:04
  • @2426021684, I don't believe `~` can be partially applied, but you might be able to make that general approach work. – dfeuer Dec 14 '16 at 19:45
  • @dfeuer It can be partially applied. – michaelmesser Dec 14 '16 at 19:47
  • 1
    @2426021684, I believe I have a fully general solution: http://stackoverflow.com/questions/41178589/is-there-a-general-way-to-apply-constraints-to-a-type-application/41178590#41178590 – dfeuer Dec 16 '16 at 06:44
7

This is a known issue. GHC is choking up because you have introduced a new type variable b not mentioned anywhere else in the instance head. One workaround is to use type families and constraint kinds.

{-# LANGUAGE ConstraintKinds, TypeFamilies, UndecideableInstances, 
             UndecideableSuperclasses, FlexibleInstances
  #-}

import GHC.Exts (Constraint)
import GHC.Prim (Any)

type family MaybeEq x :: Constraint where
  MaybeEq (Maybe a) = Eq a
  MaybeEq _         = Any    -- A good "unsatisfiable" constraint

class MaybeEq a => K a where
instance MaybeEq a => K a where
Alec
  • 31,829
  • 7
  • 67
  • 114
  • I am very surprised that this works. It seems like this ought to allow us to write `foo :: K Int => () -> Int; foo x = x` since `K Int` implies `MaybeEq Int`, which implies `() ~ Int`. Yet it doesn't. Why not? – Daniel Wagner Dec 13 '16 at 00:27
  • @DanielWagner I'm working in 8.0.1 right now and I can define such a `foo` without problem (naturally I can't _use_ it since there is no instance for `K Int`). What version are you running? – Alec Dec 13 '16 at 01:00
  • `rf2 :: Test K -> Maybe Bool` `rf2 (Test o) = (==) <$> o <*> o -- I need GHC to infer that o is Maybe Eq` – michaelmesser Dec 13 '16 at 01:16
  • Error : `• Could not deduce: a ~ Maybe a0 from the context: K a` – michaelmesser Dec 13 '16 at 01:17
  • @Alec I am also in 8.0.1. When I write `let foo :: K Int => () -> Int; foo x = x` in ghci I get `Couldn't match expected type ‘Int’ with actual type ‘()’ In the expression: x`. – Daniel Wagner Dec 13 '16 at 02:14
  • @DanielWagner Huh. Something seems amiss. Some clarifications: I'm actually in `8.0.1.20161117`, and I am both able to get the error message and avoiding it (depending on extensions enabled I think?) - still trying to whittle down a minimal test case... – Alec Dec 13 '16 at 02:32