Coercible solver does not look through "class newtypes"
The code below makes use of the "class newtype" design pattern:
class Show a => MyShow a
instance Show a => MyShow a
MyShow
is a newtype around Show
in the sense that when compiled to Core, a MyShow
dictionary is literally a newtype around Show
. Unfortunately, this newtype treatment does not extend to the Coercible
solver, as the following example demonstrates:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a -> a -> String)
newtype T2 a = MkT2 (MyShow a => a -> a -> String)
f :: T1 a -> T2 a
f = coerce
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a -> T2 a (bound at Bug.hs:20:1)
|
20 | f = coerce
| ^^^^^^
Somewhat surprisingly, this does not work. Even the error message indicates that MyShow
is a newtype (which is a bit odd, but whatever), but since the internal C:MyShow
constructor is not exposed, the Coercible
solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
-import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ -577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co -> (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+ | isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co -> (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
| otherwise
= NS_Done
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by Generic Programming of All Kinds):
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T -> TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)
-----
infixr 5 :&&:
data LoT :: Type -> Type where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
type family HeadLoT (tys :: LoT (k -> k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type -> Type -> Type where
VZ :: TyVar (x -> xs) x
VS :: TyVar xs k -> TyVar (x -> xs) k
data Atom :: Type -> Type -> Type where
Var :: TyVar d k -> Atom d k
Kon :: k -> Atom d k
(:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
(:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type
ForAllQ :: Atom (d1 -> d) Constraint -> Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint -> Atom d Type -> LoT d -> Type where
SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type -> LoT d -> Type where
Field :: { unField :: Interpret t x } -> Field t x
f
will not typecheck without the ability to coerce from ForAllQI f tys
to forall t. WrappedQI f (t ':&&: tys)
. Moreover, it would be extremely difficult to write f
without coerce
.