Note [Decomposing newtypes a bit more aggressively]
IMPORTANT: the ideas in this Note are *not* implemented. Instead, the current approach is detailed in Note [Decomposing newtype equalities] and Note [Unwrap newtypes first]. For more details about the ideas in this Note see * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549 * issue #22441 * discussion on !9282. Consider [G] c, [W] (IO Int) ~R (IO Age) where IO is abstract, and newtype Age = MkAge Int -- Not abstract With the above rules, if there any Given Irreds, the Wanted is insoluble because we can't decompose it. But in fact, if we look at the defn of IO, roughly, newtype IO a = State# -> (State#, a) we can see that decomposing [W] (IO Int) ~R (IO Age) to [W] Int ~R Age definitely does not lose completeness. Why not? Because the role of IO's argment is representational. Hence: DecomposeNewtypeIdea: decompose [W] (N s1 .. sn) ~R (N t1 .. tn) if the roles of all N's arguments are representational If N's arguments really /are/ representational this will not lose completeness. Here "really are representational" means "if you expand all newtypes in N's RHS, we'd infer a representational role for each of N's type variables in that expansion". See Note [Role inference] in GHC.Tc.TyCl.Utils. But the user might /override/ a phantom role with an explicit role annotation, and then we could (obscurely) get incompleteness. Consider module A( silly, T ) where newtype T a = MkT Int type role T representational -- Override phantom role silly :: Coercion (T Int) (T Bool) silly = Coercion -- Typechecks by unwrapping the newtype data Coercion a b where -- Actually defined in Data.Type.Coercion Coercion :: Coercible a b => Coercion a b module B where import A f :: T Int -> T Bool f = case silly of Coercion -> coerce Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose, we'll get stuck with (Int ~R Bool). Instead we want to use the [G] (T Int) ~R (T Bool), which will be in the Irreds. Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very obscure incompleteness (above). But no one is reporting a problem from the lack of decompostion, so we'll just leave it for now. This long Note is just to record the thinking for our future selves.
References 3
- Decomposing newtype equalities GHC.Tc.Solver.Equality
- Unwrap newtypes first GHC.Tc.Solver.Equality
- Role inference GHC.Tc.TyCl.Utils
Referenced by 1
- Decomposing newtype equalities GHC.Tc.Solver.Equality