type error with the program in issue #3

[LeventErkok]

when I load the program Dylan put in issue #3, I actually get a bunch of type-checking errors unless I put an explicit annotation zero : [1] in the expression z'.

The constraints look solvable to me, but maybe a rewrite is missing? Here's what I get:

error] at T.cry:5:11--5:39:
  Unsolved constraint:
    33 >= ?i3 + 0
      arising from
      matching types
      at T.cry:5:11--5:39
  where
  ?i3 is 1st type parameter
         of expression (#)
         at T.cry:5:22--5:23
[error] at T.cry:5:16--5:39:
  Unsolved constraint:
    ?i3 + (33 - ?i3) >= ?b3 + 0
      arising from
      matching types
      at T.cry:5:16--5:39
  where
  ?b3 is 1st type parameter
         of expression (#)
         at T.cry:5:35--5:36
  ?i3 is 1st type parameter
         of expression (#)
         at T.cry:5:22--5:23
[error] at T.cry:5:35--5:36:
  Unsolved constraint:
    fin ?b3
      arising from
      use of expression (#)
      at T.cry:5:35--5:36
  where
  ?b3 is 1st type parameter
         of expression (#)
         at T.cry:5:35--5:36
[error] at T.cry:2:1--5:39:
  Unsolved constraint:
    32 == ?i3 + (33 - ?i3) - ?b3
      arising from
      matching types
      at T.cry:2:1--5:39
  where
  ?b3 is 1st type parameter
         of expression (#)
         at T.cry:5:35--5:36
  ?i3 is 1st type parameter
         of expression (#)
         at T.cry:5:22--5:23
[error] at T.cry:2:1--5:39:
  Unsolved constraint:
    32 == 33 - ?i3
      arising from
      matching types
      at T.cry:2:1--5:39
  where
  ?i3 is 1st type parameter
         of expression (#)
         at T.cry:5:22--5:23

[dylanmc]

Iavor is about to replace the type-checking constraint solver, so it should be okay with this code "real soon now".

[kiniry]

We'll relate this to #36 and assign to @yav to double-check.

[yav]

Relevant example from closed issue 083.

x : ([31], [31]) -> [32]
x (y, z) = w
  where w = (zero # y) + (zero # z)

[elliottt]

I reworked the typechecker to check against signatures when present, and infer types when they're not. This change means that the type information for the arguments in the example @yav provided is present immediately, instead of when the signature is being checked after inference.

[acfoltzer]

@elliottt after these changes were merged in, we shot up to 85 test failures across the various platforms on Jenkins. It looks like most of the errors are due to being unable to typecheck take and drop from the prelude. I was thinking this was a CVC4 thing at first, as only some of our Jenkins platforms have CVC4, but it looks to be happening across the board. Thoughts?

[elliottt]

That's odd, the tests ran fine for me, which is why I merged the changes :)

[elliottt]

I just completely cleaned out my local build env, and re-ran the tests from scratch. I'm still unable to reproduce the failures that are showing up on Jenkins, so I'm at a loss as to why things aren't working there.

[elliottt]

OK, so I built master in a Fedora 20 vm, with GHC-7.8.3, and CVC4 version 1.3, and I only get 4 test failures. I think that there's something off with the Jenkins machines, we should diagnose this more on Monday :)

[elliottt]

Actually, scratch that. I get 85 failures when I remove CVC4. I'll add this to the ticket about getting CVC4 on all the Jenkins machines :)

[elliottt]

OK, so adding $CVC4 to the path as specified in #150 by @atomb has fixed the problem on build slaves that have CVC4 installed. Most are back to 4/85 failing, but the ones that lack CVC4 are still failing 85/85.