The Sigma constructor does not typecheck

[robrix]

I don’t know when this broke exactly, but Sigma no longer typechecks:

λ: runCommand (Surface.Command.Run "src/Prelude.surf")
Cannot unify A -> Type with Type

Execution trace as of 34873fb

(checkDeclaration Prelude.Sigma, { g3, [] })
(isType (A -> (A -> Type) -> Type), { g3, [] })
(isType Type, { g3, [] })
(isType ((A -> Type) -> Type), { g3, [ A :: Type ] })
(isType (A -> Type), { g3, [ A :: Type ] })
(isType A, { g3, [ A :: Type ] })
(isType Type, { g3, [ A :: Type ] })
(isType Type, { g3, [ A :: Type, _ :: A ] })
(isType Type, { g3, [ A :: Type, B :: (A -> Type) ] })
(checkConstructor Prelude.Sigma.sigma, { g3, [] })
(fresh Type, { g3, [ ; ] })
(fresh (A -> Type), { h3, [ ;, g3 := Type ] })
(infer (A -> (B : (A -> Type)) -> (a : A) -> B a -> Sigma A B), { i3, [ ;, g3 := Type, h3 := (A -> Type) ] })
(infer ((B : (A -> Type)) -> (a : A) -> B a -> Sigma A B), { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type ] })
(infer ((a : A) -> B a -> Sigma A B), { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type) ] })
(infer (B a -> Sigma A B), { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A ] })
(infer (Sigma A B), { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a ] })
(infer B, { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a ] })
(fresh A, { i3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a ] })
(fresh _, { j3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A ] })
(check (Sigma A) (Type -> j3), { k3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(infer (Sigma A), { k3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(infer A, { k3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(fresh _, { k3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(check Sigma (Type -> k3), { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := _ ] })
(unify (A -> (A -> Type) -> Type) (Type -> k3), { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := _ ] })
(unify Type Type, { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := _ ] })
(unify ((A -> Type) -> Type) k3, { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := _ ] })
(solve k3 [] ((A -> Type) -> Type), { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := _ ] })
(replace [ k3 := ((A -> Type) -> Type) ], { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(unify (Type -> j3) k3, { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := ((A -> Type) -> Type) ] })
(solve k3 [] (Type -> j3), { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _, k3 := ((A -> Type) -> Type) ] })
(unify ((A -> Type) -> Type) (Type -> j3), { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
(unify (A -> Type) Type, { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })
([ "Cannot unify A -> Type with Type", "" ], { l3, [ ;, g3 := Type, h3 := (A -> Type), A :: Type, B :: (A -> Type), a :: A, _ :: B a, i3 := A, j3 := _ ] })