## 2+2=4

I just had the following interaction with the version I just pushed:

`*ParseEvalCheckRender> parseit synthit`

input:

Nat => => data X : * where <z> : X ; <s> : all x : X => X

two => => <s <s <z>>> : Nat

plus => => lam m => lam n => m elim{Nat} (lam x => Nat)

% n

% (lam x => lam xh => <s xh>) :

% all m : Nat => all n : Nat => Nat

---

plus two two

STOP

`<s <s <s <s <z>>>>>`

data X : * where <z> : X ; <s> : all x : X => X

Some sort of progress, I think.

January 15th, 2006 at 8:11 pm

Further to that, I just added a tests directory with that stuff in it. More tomorrow, but a good day’s work from the team, I think. Cheers guys!

January 17th, 2006 at 11:08 am

What’s wrong with this? (I do not mean the crumbled logo)

$ ghci -fallow-overlapping-instances ParseEvalCheckRender.lhs

___ ___ _

/ _ \ /\ /\/ __(_)

/ /_\// /_/ / / | | GHC Interactive, version 6.2.2, for Haskell 98.

/ /_\\/ __ / /___| | http://www.haskell.org/ghc/

\____/\/ /_/\____/|_| Type for help.

Loading package base … linking … done.

Compiling Monoid ( ./Monoid.hs, interpreted )

Compiling Applicative ( ./Applicative.hs, interpreted )

Compiling Traversable ( ./Traversable.hs, interpreted )

Compiling Idiomatics ( ./Idiomatics.lhs, interpreted )

./Idiomatics.lhs:202:

Overlapping instance declarations:

./Idiomatics.lhs:202: AppHom Id f

./Idiomatics.lhs:252: AppHom a (Coprod b a)

./Idiomatics.lhs:214:

Overlapping instance declarations:

./Idiomatics.lhs:214: AppHom g (Comp f g)

./Idiomatics.lhs:216: AppHom f (Comp f g)

Failed, modules loaded: Traversable, Applicative, Monoid.

*Traversable>

January 17th, 2006 at 11:53 am

I’d guess that your ghc version being more eager than ours, however word from Conor is that if you delete those instances for it’ll work, we don’t use the more exotic kit in the file.

The reason your flags don’t fix it is we’ve added pragmas at the top of all our files which overrule your options and enforce ours.

January 18th, 2006 at 6:21 am

It’s was due to Djinn. It’s dependency on the IntMap lib made me grab for an unstable deb archive of ghc’s.

I didn’t understand this warning:

/Idiomatics.lhs:214:

Overlapping instance declarations:

./Idiomatics.lhs:214: AppHom g (Comp f g)

./Idiomatics.lhs:216: AppHom f (Comp f g)

as these instances had already been commented out.

And deleting instance declarations beginning at lines 202 and 252 in Idiomatics as you say evoked more overlapping-instances-warnings in Term.

./Term.lhs:212:

Overlapping instance declarations:

./Term.lhs:212: Eliminable t (Bwd e)

./Term.lhs:227: Eliminable (Synth x) x

./Term.lhs:216:

Overlapping instance declarations:

./Term.lhs:216: Eliminable t (Fwd e)

./Term.lhs:227: Eliminable (Synth x) x

./Term.lhs:220:

Overlapping instance declarations:

./Term.lhs:220: Eliminable (Synth x) Icit

./Term.lhs:227: Eliminable (Synth x) x

./Term.lhs:224:

Overlapping instance declarations:

./Term.lhs:224: Eliminable x (y, z)

./Term.lhs:227: Eliminable (Synth x) x

But i can live with that for the moment. It’s just that the session log had made me curious. Thank you ☺

January 18th, 2006 at 1:11 pm

Hehe, yes well, luckily 6.4.1 only complains when it has to decide between overlapping instances and since the x in (Synth x) is never set to Bwd Fwd (,) or Icits we’re OK