data instance T [a] where
T1 :: forall b. b -> T [Maybe b]
-Hence
- Co7T a :: T [a] ~ :R7T a
-Now we want
+Hence we translate to
-- Wrapper
$WT1 :: forall b. b -> T [Maybe b]
-- Worker
T1 :: forall c b. (c ~ Maybe b) => b -> :R7T c
+ -- Coercion from family type to representation type
+ Co7T a :: T [a] ~ :R7T a
+
\begin{code}
mkDataConIds :: Name -> Name -> DataCon -> DataConIds
mkDataConIds wrap_name wkr_name data_con