Task: rid TypeChecking.Pretty of UndecidableInstances

[GoogleCodeExporter]

See Agda.TypeChecking.Pretty:

{-# LANGUAGE UndecidableInstances #-}

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Named_ a) where
    prettyTCM x = prettyA =<< reify x

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Arg a) where
    prettyTCM x = prettyA =<< reify x

instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Dom a) where
    prettyTCM x = prettyA =<< reify x

The PrettyTCM instances for Named_, Arg, and Dom should be defined in terms of
PrettyTCM a, not Reify a.

How to implement this?

Write functions that put the information contained in Named_ / Arg_/ Dom onto a
Doc, like

  prettyArg :: Arg Doc -> Doc

and then just define

  prettyTCM arg = prettyArg <$> prettyTCM (unArg arg)

Similar functionality can be found in Syntax.Concrete.Pretty:

pHidden :: Pretty a => ArgInfo -> a -> Doc
pHidden i = bracks h . pretty
  where bracks Hidden   = braces'
        bracks Instance = dbraces
        bracks NotHidden= id
        h = argInfoHiding i

pRelevance :: Pretty a => ArgInfo -> a -> Doc
pRelevance i a =
  let d = pretty a
  in  if render d == "_" then d else pretty (argInfoRelevance i) <> d

Original issue reported on code.google.com by andreas....@gmail.com on 9 Oct 2014 at 10:19