type applications should start with a type atom

[athanclark]

I'm not exactly sure what this means, but it happened during type inference for this function:

chunks : Int -> List a -> List (List a)
chunks n xs =
  let go : (List a, List (List a)) -> a -> (List a, List (List a))
      go (acc, ys) x =
        let size = List.length acc
        in  if size < n
            then (List.append acc (x::[]), ys)
            else ([]                     , List.append ys (acc::[]))
      (zs, zss) = List.foldl go ([],[]) xs
  in  List.append zss (zs :: [])

I've tried a number of tricks to adjust the terms, but for some reason it's not getting the system to work properly. Any ideas what I'm doing wrong here?

[jvoigtlaender]

Your problem is that you assume List.foldl has type (b -> a -> b) -> b -> List a -> b, but it has type (a -> b -> b) -> b -> List a -> b.

[athanclark]

Ahh okay, but that should just cause a type mismatch, not throw a wrench in its spokes :\

Do you know what unification algorithm elm uses? It can't be just AlgorithmW is it? Is there a specific paper they modeled after, like bottom-up or outside-in?

[jvoigtlaender]

You are right that this should be reported as a type mismatch. That it instead crashes the compiler is a compiler bug. A compiler bug that has been reported repeatedly (and doesn't really need an additional issue here in this repository, I think). Look, for example, at: elm/compiler#1326, elm/compiler#1231, #105.

About your questions: No, I don't know. My impression from some cursory look into the type checking code a while ago was that unification was done in a quite ad-hoc way. But I may be wrong, and there may actually be a specific known algorithm followed there.

[rtfeldman]

Closing in favor of elm/compiler#1231