newtype with gadt-like constraint

153 Views Asked by At

I understand why you can't do this:

{-# LANGUAGE GADTs  #-}

newtype NG a  where MkNG :: Eq a => a -> NG a

-- 'A newtype constructor cannot have a context in its type', says GHC

That's because the 'data' constructor MkNG is not really a constructor. "The constructor N in an expression coerces a value from type t to type ..." says the language report, Section 4.2.3 "Unlike algebraic datatypes, the newtype constructor N is unlifted, ..."

If it were to be able to support a constraint, it would need an argument position for the constraint's dictionary.

Now I've got your attention I'm going to ask about that deprecated feature, for which you often see (very old) StackOverflow answers saying to use GADTs instead:

{-# LANGUAGE DatatypeContexts  #-}             -- deprecated ~2010

newtype Eq a => NC a = MkNC a                  -- inferred MkNC :: Eq a => a -> NC a

-- nc = MkNC (id :: Int -> Int)                -- rejected no Eq instance

quux (MkNC _) = ()                             -- inferred quux :: Eq a => NC a -> ()
quuz (x :: NC a) = ()                          -- inferred quuz :: NC a -> ()

(That type for quuz is one of the annoyances with DatatypeContexts: because the constructor doesn't appear in the pattern match, type inference can't 'see' the constraint.)

So this works (or doesn't depending on your point of view) just as well (or badly) as DatatypeContexts on data types.

My question is: how? MkNC again just coerces a value/is unlifted. Does it use dictionary-passing to apply the constraint? Where does the dictionary slot in, given that the coercion is purely a compile-time effect?

0

There are 0 best solutions below