That&#39;s really nice. Very interesting. Thank you.<br><br><div class="gmail_quote">On Fri, Jun 25, 2010 at 9:55 PM, Edward Kmett <span dir="ltr">&lt;<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">I&#39;ve obtained permission to repost Gershom&#39;s slides on how to deserialize GADTs by typechecking them yourself, which are actually a literate haskell source file, that he was rendering to slides. Consequently, I&#39;ve just pasted the content below as a literate email.<br>

<br>-Edward Kmett<br><br>-<br>Deserializing strongly typed values<br><br>(four easy pieces about typechecking)<br><br>Gershom Bazerman<br><br>-<br>prior art:<br>Oleg (of course)<br><a href="http://okmij.org/ftp/tagless-final/course/course.html" target="_blank">http://okmij.org/ftp/tagless-final/course/course.html</a><br>

<br>...but also<br>Stephanie Weirich<br><a href="http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs" target="_blank">http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs</a><br><br>=<br>Ahem...<br>\begin{code}<br>{-# LANGUAGE DeriveDataTypeable,<br>

             ExistentialQuantification,<br>             FlexibleContexts,<br>             FlexibleInstances,<br>             FunctionalDependencies,<br>             GADTs,<br>             RankNTypes,<br>             ScopedTypeVariables<br>

 #-}<br>\end{code}<br>=<br>ahem.<br>\begin{code}<br>import Data.Typeable<br>import Data.Maybe<br>import Control.Monad.Error<br>import Control.Applicative<br>import qualified Data.Map as M<br>import Unsafe.Coerce<br>\end{code}<br>

=<br>A simple ADT.<br><br>\begin{code}<br>data SimpleExpr = SOpBi String SimpleExpr SimpleExpr<br>                | SOpUn String SimpleExpr<br>                | SDbl Double<br>                | SBool Bool deriving (Read, Show, Typeable)<br>

<br>\end{code}<br>Yawn.<br>=<br>An awesome GADT!<br><br>\begin{code}<br>data Expr a where<br>    EDbl  :: Double -&gt; Expr Double<br>    EBool :: Bool -&gt; Expr Bool<br>    EBoolOpBi :: BoolOpBi -&gt; Expr Bool -&gt; Expr Bool -&gt; Expr Bool<br>

    ENumOpBi  :: NumOpBi -&gt; Expr Double -&gt; Expr Double -&gt; Expr Double<br>    ENumOpUn  :: NumOpUn -&gt; Expr Double -&gt; Expr Double<br>                 deriving Typeable<br><br>data NumOpBi = Add | Sub deriving (Eq, Show)<br>

data NumOpUn = Log | Exp deriving (Eq, Show)<br>data BoolOpBi = And | Or deriving (Eq, Show)<br>\end{code}<br><br>The GADT is well typed. It cannot go wrong.<br>-<br>It also cannot derive show.<br>=<br>But we can write show...<br>

<br>\begin{code}<br>showIt :: Expr a -&gt; String<br>showIt (EDbl d) = show d<br>showIt (EBool b) = show b<br>showIt (EBoolOpBi op x y) = &quot;(&quot; ++ show op<br>                            ++ &quot; &quot; ++ showIt x<br>

                            ++ &quot; &quot; ++ showIt y ++ &quot;)&quot;<br>showIt (ENumOpBi op x y)  = &quot;(&quot; ++ show op<br>                            ++ &quot; &quot; ++ showIt x<br>                            ++ &quot; &quot; ++ showIt y ++ &quot;)&quot;<br>

showIt (ENumOpUn op x) = show op ++ &quot;(&quot; ++ showIt x ++ &quot;)&quot;<br>\end{code}<br>=<br>And eval is *much nicer*.<br>It cannot go wrong --&gt; no runtime typechecks.<br><br>\begin{code}<br>evalIt :: Expr a -&gt; a<br>

evalIt (EDbl x) = x<br>evalIt (EBool x) = x<br>evalIt (EBoolOpBi op expr1 expr2)<br>       | op == And = evalIt expr1 &amp;&amp; evalIt expr2<br>       | op == Or  = evalIt expr2 || evalIt expr2<br><br>evalIt (ENumOpBi op expr1 expr2)<br>

       | op == Add = evalIt expr1 + evalIt expr2<br>       | op == Sub = evalIt expr1 - evalIt expr2<br>\end{code}<br>=<br>But how do we write read!?<br><br>read &quot;EBool False&quot; = Expr Bool<br>read &quot;EDbl 12&quot; = Expr Double<br>

<br>The type being read depends on the content of the string.<br><br>Even worse, we want to read not from a string that looks obvious<br>to Haskell (i.e. a standard showlike instance) but from<br>something that looks pretty to the user -- we want to *parse*.<br>

<br>So we parse into our simple ADT.<br><br>Then we turn our simple ADT into our nice GADT.<br>-<br>But how?<br><br>How do we go from untyped... to typed?<br><br>[And in general -- not just into an arbitrary GADT,<br>but an arbitrary inhabitant of a typeclass.]<br>

<br>[i.e. tagless final, etc]<br><br>=<br>Take 1:<br>Even if we do not know what type we are creating,<br>we eventually will do something with it.<br><br>So we paramaterize our typechecking function over<br>an arbitrary continuation.<br>

<br>\begin{code}<br>mkExpr :: (forall a. (Show a, Typeable a) =&gt; Expr a -&gt; r) -&gt; SimpleExpr -&gt; r<br>mkExpr k expr = case expr of<br>                   SDbl d  -&gt; k $ EDbl d<br>                   SBool b -&gt; k $ EBool b<br>

                   SOpUn op expr1 -&gt; case op of<br>                      &quot;log&quot; -&gt; k $ mkExpr&#39; (ENumOpUn Log) expr1<br>                      &quot;exp&quot; -&gt; k $ mkExpr&#39; (ENumOpUn Exp) expr1<br>

                      _ -&gt; error &quot;bad unary op&quot;<br>                   SOpBi op expr1 expr2 -&gt; case op of<br>                      &quot;add&quot; -&gt; k $ mkExprBi (ENumOpBi Add) expr1 expr2<br>                      &quot;sub&quot; -&gt; k $ mkExprBi (ENumOpBi Sub) expr1 expr2<br>

\end{code}<br>=<br>Where&#39;s the typechecking?<br><br>\begin{code}<br>mkExpr&#39; k expr = mkExpr (appCast $ k) expr<br><br><br>mkExprBi k expr1 expr2 = mkExpr&#39; (mkExpr&#39; k expr1) expr2<br><br><br>appCast :: forall a b c r. (Typeable a, Typeable b) =&gt; (c a -&gt; r) -&gt; c b -&gt; r<br>

appCast f x = maybe err f $ gcast x<br>    where err = error $ &quot;Type error. Expected: &quot; ++ show (typeOf (undefined::a))<br>                ++ &quot;, Inferred: &quot; ++ show (typeOf (undefined::b))<br>\end{code}<br>

<br>... We let Haskell do all the work!<br>=<br>Hmmm... the continuation can be anything.<br>So let&#39;s just make it an existential constructor.<br><br>\begin{code}<br>data ExprBox = forall a. Typeable a =&gt; ExprBox (Expr a)<br>

<br>appExprBox :: (forall a. Expr a -&gt; res) -&gt; ExprBox -&gt; res<br>appExprBox f (ExprBox x) = f x<br><br>tcCast :: forall a b c. (Typeable a, Typeable b) =&gt; Expr a -&gt; Either String (Expr b)<br>tcCast x = maybe err Right $ gcast x<br>

    where err = Left $ &quot;Type error. Expected: &quot; ++ show (typeOf (undefined::a))<br>                ++ &quot;, Inferred: &quot; ++ show (typeOf (undefined::b))<br>\end{code}<br><br>Now we can delay deciding what to apply until later.<br>

Typecheck once, execute repeatedly!<br><br>=<br>One more trick -- monadic notation lets us<br>extend the context of unpacked existentials<br>to the end of the do block<br><br>\begin{code}<br>retBox x = return (ExprBox $ x, typeOf x)<br>

<br>typeCheck :: SimpleExpr -&gt; Either String (ExprBox, TypeRep)<br>typeCheck (SDbl d) = retBox (EDbl d)<br>typeCheck (SBool b) = retBox (EBool b)<br>typeCheck (SOpBi op s1 s2) = case op of<br>           &quot;add&quot; -&gt; tcBiOp (ENumOpBi Add)<br>

           &quot;sub&quot; -&gt; tcBiOp (ENumOpBi Sub)<br>           &quot;and&quot; -&gt; tcBiOp (EBoolOpBi And)<br>           &quot;or&quot;  -&gt; tcBiOp (EBoolOpBi Or)<br>    where<br>      tcBiOp constr = do<br>        (ExprBox e1, _) &lt;- typeCheck s1<br>

        (ExprBox e2, _) &lt;- typeCheck s2<br>        e1&#39; &lt;- tcCast e1<br>        e2&#39; &lt;- tcCast e2<br>        retBox $ constr e1&#39; e2&#39;<br>\end{code}<br>=<br>So that&#39;s fine for *very* simple expressions.<br>

How does it work for interesting GADTs?<br>(like, for example, HOAS)?<br><br>(The prior art doesn&#39;t demonstrate HOAS --<br> it uses DeBruijn.)<br>=<br>Our simple world<br><br>\begin{code}<br>type Ident = String<br>type TypeStr = String<br>

<br>data STerm = SNum Double<br>             | SApp STerm STerm<br>             | SVar Ident<br>             | SLam Ident TypeRep STerm<br>\end{code}<br><br>Note.. terms are Church style -- each var introduced<br>has a definite type.<br>

<br>Determining this type is left as an exercise.<br><br>=<br>Over the rainbow in well-typed land.<br><br>\begin{code}<br>data Term a where<br>    TNum :: Double -&gt; Term Double<br>    TApp :: Term (a -&gt; b) -&gt; Term a -&gt; Term b<br>

    TLam :: Typeable a =&gt; (Term a -&gt; Term b) -&gt; Term (a -&gt; b)<br>    TVar :: Typeable a =&gt; Int -&gt; Term a<br>            deriving Typeable<br>\end{code}<br><br>Wait! DeBrujin (TVar) *and* HOAS (TLam)! The worst of both worlds.<br>

<br>Don&#39;t worry. In the final product all TVars are eliminated by construction.<br><br>Exercise to audience: rewrite the code so that TVar can be eliminated<br>from the Term type.<br>=<br>Show and eval...<br><br>\begin{code}<br>

showT :: Int -&gt; Term a -&gt; String<br>showT c (TNum d) = show d<br>showT c (TApp f x) = &quot;App (&quot; ++ showT c f<br>                     ++ &quot;) (&quot; ++ showT c x ++ &quot;)&quot;<br>showT c (TLam f)   = &quot;Lam &quot; ++ (&quot;a&quot;++show c)<br>

                     ++  &quot; -&gt; &quot; ++ (showT (succ c) $ f (TVar c))<br>showT c (TVar i)   = &quot;a&quot;++show i<br><br>runT :: Term a -&gt; Term a<br>runT (TNum d) = (TNum d)<br>runT (TLam f) = (TLam f)<br>runT (TApp f x) = case runT f of TLam f&#39; -&gt; runT (f&#39; x)<br>

runT (TVar i) = error (show i)<br>\end{code}<br>=<br>The existential<br><br>\begin{code}<br>data TermBox = forall a. Typeable a =&gt; TermBox (Term a)<br>appTermBox :: (forall a. Typeable a =&gt; Term a -&gt; res) -&gt; TermBox -&gt; res<br>

appTermBox f (TermBox x) = f x<br>\end{code}<br>=<br>The typechecker returns a box *and* a typeRep.<br><br>Cast is the usual trick.<br><br>\begin{code}<br>retTBox :: Typeable a =&gt; Term a -&gt; Either String (TermBox, TypeRep)<br>

retTBox x = return (TermBox $ x, typeOf x)<br><br>type Env = M.Map Ident (TermBox, TypeRep)<br><br>trmCast :: forall a b c. (Typeable a, Typeable b) =&gt;<br>           Term a -&gt; Either String (Term b)<br>trmCast x = maybe err Right $ gcast x<br>

    where err = Left $ &quot;Type error. Expected: &quot; ++<br>                show (typeOf (undefined::a))<br>                ++ &quot;, Inferred: &quot; ++<br>                show (typeOf (undefined::b))<br>\end{code}<br>

<br>=<br>\begin{code}<br>typeCheck&#39; :: STerm -&gt; Env -&gt; Either String (TermBox, TypeRep)<br>typeCheck&#39; t env = go t env 0<br>    where<br>      go (SNum d) _ idx = retTBox (TNum d)<br>      go (SVar i) env idx = do<br>

        (TermBox t, _) &lt;- maybe (fail $ &quot;not in scope: &quot; ++ i)<br>                          return $ M.lookup i env<br>        retTBox $ t<br>\end{code}<br><br>Nums and vars are easy.<br>=<br>App and Lam... less so.<br>

<br>\begin{code}<br>      go (SApp s1 s2) env idx = do<br>        (TermBox e1, tr1) &lt;- go s1 env idx<br>        (TermBox e2, _) &lt;- go s2 env idx<br>        TermBox rt &lt;- return $ mkTerm $ head $ tail $<br>                      typeRepArgs $ head $ typeRepArgs $ tr1<br>

                      -- TypeReps have their... drawbacks.<br>        e1&#39; &lt;- trmCast e1<br>        retTBox $ TApp e1&#39; e2 `asTypeOf` rt<br>      go (SLam i tr s) env idx = do<br>        TermBox et &lt;- return $ mkTerm tr<br>

        (TermBox e, _) &lt;- go s<br>                           (M.insert i<br>                                (TermBox (TVar idx `asTypeOf` et),tr)<br>                                env<br>                           )<br>

                           (idx + 1)<br>        retTBox $ TLam (\x -&gt; subst (x `asTypeOf` et) idx e)<br>\end{code}<br>=<br>How does mkTerm work?<br><br>\begin{code}<br>mkTerm :: TypeRep -&gt; TermBox<br>mkTerm tr = go tr TermBox<br>

    where<br>      go :: TypeRep -&gt; (forall a. (Typeable a) =&gt; Term a -&gt; res) -&gt; res<br>      go tr k<br>          | tr == typeOf (0::Double) = k (TNum 0)<br>          | typeRepTyCon tr == arrCon =<br>                 go (head $ typeRepArgs tr)<br>

                 $ \xt -&gt; go (head $ tail $ typeRepArgs tr)<br>                 $ \y -&gt; k (TLam $ \x -&gt; const y (x `asTypeOf` xt))<br><br>      arrCon = typeRepTyCon $ typeOf (undefined::Int -&gt; String)<br>\end{code}<br>

<br>Same principle -- but can build arrows directly.<br><br>Doing so requires staying cps... I think.<br>=<br>And this is how we get rid of the DeBruijn terms.<br><br>\begin{code}<br>subst :: (Typeable a) =&gt; Term a -&gt; Int -&gt; Term b -&gt; Term b<br>

subst t i trm = go trm<br>    where<br>      go :: Term c -&gt; Term c<br>      go (TNum d) = (TNum d)<br>      go (TApp f x) = TApp (go f) (go x)<br>      go (TLam f) = TLam (\a -&gt; go (f a))<br>      go (TVar i&#39;)<br>

         | i == i&#39; = either error id $ trmCast t<br>         | otherwise = (TVar i&#39;)<br>\end{code}<br><br>Q: Now you see why DeBruijn is handy -- substitution<br>is otherwise a pain.<br><br>=<br>But note -- all functions must be monotyped.<br>

This is the simply typed lambda calculus.<br><br>How do we represent TLam (\a -&gt; a)?<br><br>The masses demand HM polymorphism.<br>-<br><br>Take 4:<br><br>A damn dirty hack.<br><br>=<br>All hacks begin with Nats.<br><br>

\begin{code}<br>data Z = Z deriving (Show, Typeable)<br>data S a = S a deriving (Show, Typeable)<br>\end{code}<br>=<br>typeCheck is almost the same.<br><br>\begin{code}<br>typeCheck&#39;&#39; :: STerm -&gt; Env -&gt; Either String (TermBox, TypeRep)<br>

typeCheck&#39;&#39; t env = go t env 0<br>    where<br>      go :: STerm -&gt; Env -&gt; Int -&gt; Either String (TermBox, TypeRep)<br>      go (SNum d) _ idx = retTBox (TNum d)<br>      go (SVar i) env idx = do<br>        (TermBox t, _) &lt;- maybe (fail $ &quot;not in scope: &quot; ++ i)<br>

                          return $ M.lookup i env<br>        retTBox $ t<br>\end{code}<br>=<br>\begin{code}<br>      go (SApp s1 s2) env idx = do<br>        (TermBox e1, tr1) &lt;- go s1 env idx<br>        (TermBox e2, _) &lt;- go s2 env idx<br>

        TermBox rt  &lt;- unifyAppRet e1 e2<br>        e1&#39; &lt;- unifyAppFun e1 e2<br>        retTBox $ TApp e1&#39; e2 `asTypeOf` rt<br>      go (SLam i tr s) env idx = do<br>        TermBox et &lt;- return $ mkTerm&#39; $ tr<br>

        (TermBox e, _) &lt;- go s (M.insert i<br>                                (TermBox (TVar idx `asTypeOf` et),tr)<br>                                env)<br>                               (idx + 1)<br>        retTBox $ TLam (\x -&gt; subst (x `asTypeOf` et) idx e)<br>

\end{code}<br><br>It looks like we just factored on the nasty arrow code.<br>=<br>mkTerm is almost the same... we just extended it to deal with Nats.<br>\begin{code}<br>mkTerm&#39; :: TypeRep -&gt; TermBox<br>mkTerm&#39; tr = go tr TermBox<br>

    where<br>      go :: TypeRep -&gt; (forall a. (Typeable a) =&gt; Term a -&gt; res) -&gt; res<br>      go tr k<br>          | tr == typeOf (0::Double) = k (TNum 0)<br>          | tr == typeOf Z = k (TVar 0 :: Term Z)<br>

          | typeRepTyCon tr == succCon = go (head $ typeRepArgs tr)<br>                               $ \t -&gt; k $ succTerm t<br>          | isArr tr =<br>                 go (head $ typeRepArgs tr)<br>                 $ \xt -&gt; go (head $ tail $ typeRepArgs tr)<br>

                 $ \y -&gt; k (TLam $ \x -&gt; const y (x `asTypeOf` xt))<br>          | otherwise = error $ show tr<br><br>      succCon = typeRepTyCon $ typeOf (S Z)<br>      succTerm :: Typeable b =&gt; Term b -&gt; Term (S b)<br>

      succTerm _ = TVar 0<br>\end{code}<br>=<br>Some utilities<br>\begin{code}<br>isArr :: TypeRep -&gt; Bool<br>isArr x = typeRepTyCon x == (typeRepTyCon $ typeOf (undefined::Int -&gt; String))<br><br>splitArrCon :: TypeRep -&gt; Either String (TypeRep, TypeRep)<br>

splitArrCon x<br>    | isArr x = case typeRepArgs x of<br>                  [a,b] -&gt; Right (a,b)<br>                  _ -&gt; Left $ &quot;Expected function, inferred: &quot; ++ show x<br>    | otherwise = Left $ &quot;Expected function, inferred: &quot; ++ show x<br>

<br>\end{code}<br>=<br>Give an arrow term we unify it with its argument...<br>and return a witness.<br>\begin{code}<br>unifyAppRet :: forall a b. (Typeable a, Typeable b) =&gt;<br>               Term a -&gt; Term b -&gt; Either String TermBox<br>

unifyAppRet x y = do<br>  tr &lt;- unifyAppTyps<br>        (head $ typeRepArgs $ typeOf x)<br>        (head $ typeRepArgs $ typeOf y)<br>  return $ mkTerm&#39; tr<br><br>\end{code}<br>=<br>Yes. Actual unification.<br>(although this is unification of a type template,<br>

 so at least it is local)<br>\begin{code}<br>unifyAppTyps :: TypeRep -&gt; TypeRep -&gt; Either String TypeRep<br>unifyAppTyps trf trx = do<br>  (fl,fr) &lt;- splitArrCon trf<br>  env &lt;- go M.empty fl trx<br>  subIt env fr<br>

    where<br>      -- go yields a substitution environment.<br>      go :: M.Map String TypeRep -&gt; TypeRep -&gt;<br>            TypeRep -&gt; Either String (M.Map String TypeRep)<br>      go env x y<br>         | isFree x = case M.lookup (show x) env of<br>

                        Just x&#39; -&gt; if x&#39; == y then return env else Left (error &quot;a&quot;)<br>                        Nothing -&gt; return $ M.insert (show x) y env<br>         | isArr x = do<br>                 (lh,rh) &lt;- splitArrCon x<br>

                 (lh&#39;,rh&#39;) &lt;- splitArrCon y<br>                 env&#39; &lt;- go env lh lh&#39;<br>                 go env&#39; rh rh&#39;<br>         | otherwise = if x == y then return env else Left (error &quot;b&quot;)<br>

\end{code}<br>=<br>\begin{code}<br>      -- subIt applies it<br>      subIt :: M.Map String TypeRep -&gt; TypeRep -&gt; Either String TypeRep<br>      subIt env x<br>            | isFree x = case M.lookup (show x) env of<br>

                           Just x&#39; -&gt; return x&#39;<br>                           Nothing -&gt; Left (error &quot;c&quot;)<br>            | isArr x = do<br>                 (lh,rh) &lt;- splitArrCon x<br>                 lh&#39; &lt;- subIt env lh<br>

                 rh&#39; &lt;- subIt env rh<br>                 return $ mkTyConApp arrCon [lh&#39;,rh&#39;]<br>            | otherwise = return x<br>      succCon = typeRepTyCon $ typeOf (S Z)<br>      zCon = typeRepTyCon $ typeOf Z<br>

      isFree x = typeRepTyCon x `elem` [zCon, succCon]<br>      arrCon = (typeRepTyCon $ typeOf (undefined::Int -&gt; String))<br>\end{code}<br><br>=<br>And now, we just have to convince GHC that they unify!<br><br>\begin{code}<br>

unifyAppFun :: forall a b c. (Typeable a, Typeable b, Typeable c)<br>               =&gt; Term a -&gt; Term b -&gt; Either String (Term c)<br>unifyAppFun x y = do<br>  unifyAppTyps (head $ typeRepArgs $ typeOf x) (head $ typeRepArgs $ typeOf y)<br>

  return $ unsafeCoerce x<br>\end{code}<br>=<br>Problem solved.<br><br><br><div class="gmail_quote">On Fri, Jun 25, 2010 at 2:03 PM, Edward Kmett <span dir="ltr">&lt;<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">It turns out that defining Read is somewhat tricky to do for a GADT. <br><br>Gershom Bazerman has some very nice slides on how to survive the process by manual typechecking (much in the spirit of Oleg&#39;s meta-typechecking code referenced by Stephen&#39;s follow up below)<br>


<br>He presented them at hac-phi this time around.<br><br>I will check with him to see if I can get permission to host them somewhere and post a link to them here.<br><font color="#888888"><br>-Edward Kmett</font><div><div>

</div><div><br><br><div class="gmail_quote">On Fri, Jun 25, 2010 at 5:04 AM,  <span dir="ltr">&lt;<a href="mailto:corentin.dupont@ext.mpsa.com" target="_blank">corentin.dupont@ext.mpsa.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"><br>
Hello Haskellers,<br>
<br>
I&#39;m having trouble writing a Read Instance for my GATD.<br>
Arg this GATD!! It causes me more problems that it solves ;)<br>
Especially with no automatic deriving, it adds a lot of burden to my code.<br>
<br>
&gt;data Obs a where<br>
&gt;    ProposedBy :: Obs Int       -- The player that proposed the tested<br>
rule<br>
&gt;    Turn       :: Obs Turn      -- The current turn<br>
&gt;    Official   :: Obs Bool      -- whereas the tested rule is official<br>
&gt;    Equ        :: (Eq a, Show a, Typeable a) =&gt; Obs a -&gt; Obs a -&gt; Obs Bool<br>
&gt;    Plus       :: (Num a) =&gt; Obs a -&gt; Obs a -&gt; Obs a<br>
&gt;    Time       :: (Num a) =&gt; Obs a -&gt; Obs a -&gt; Obs a<br>
&gt;    Minus      :: (Num a) =&gt; Obs a -&gt; Obs a -&gt; Obs a<br>
&gt;    And        :: Obs Bool -&gt; Obs Bool -&gt; Obs Bool<br>
&gt;    Or         :: Obs Bool -&gt; Obs Bool -&gt; Obs Bool<br>
&gt;    Not        :: Obs Bool -&gt; Obs Bool<br>
&gt;    Konst      :: a -&gt; Obs a<br>
<br>
<br>
&gt; instance Read a =&gt; Read (Obs a) where<br>
&gt; readPrec = (prec 10 $ do<br>
&gt;        Ident &quot;ProposedBy&quot; &lt;- lexP<br>
&gt;        return (ProposedBy))<br>
&gt;     +++<br>
&gt;      (prec 10 $ do<br>
&gt;        Ident &quot;Official&quot; &lt;- lexP<br>
&gt;        return (Official))<br>
&gt;  (etc...)<br>
<br>
Observable.lhs:120:8:<br>
    Couldn&#39;t match expected type `Int&#39; against inferred type `Bool&#39;<br>
      Expected type: ReadPrec (Obs Int)<br>
      Inferred type: ReadPrec (Obs Bool)<br>
<br>
<br>
Indeed &quot;ProposedBy&quot; does not have the same type that &quot;Official&quot;.<br>
Mmh how to make it all gently mix altogether?<br>
<br>
<br>
Best,<br>
Corentin<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>
</div></div></blockquote></div><br>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br>