Universe inconsistency

[nicolabotta]

The following two files

> module HList.HList

> %default total
> %access public export
> %auto_implicits off

> ||| An heterogenous list (a list of values of possibly different types)
> data HList : List Type -> Type where
>   Nil  : HList Nil
>   (::) : {t : Type} -> {ts : List Type} -> t -> HList ts -> HList (t :: ts)

> import HList.HList

> %default total
> %access public export
> %auto_implicits off

> head : {t : Type} -> {ts : List Type} -> HList (t :: ts) -> t
> head {t} {ts} (x :: xs) = x

> tail : {t : Type} -> {ts : List Type} -> HList (t :: ts) -> HList ts
> tail {t} {ts} (x :: xs) = xs

> listProd : {ts : List Type} -> HList (map List ts) -> List (HList ts)
> listProd {ts = Nil}        _    = [Nil]
> listProd {ts = (t :: ts')} yzss = [x :: yzs | x <- (head yzss), yzs <- (listProd (tail yzss))]

type check fine in 1.3.1-git:f76dac0af. However the file

> module HList.UniverseIssue1

> %default total
> %access public export
> %auto_implicits off

> data HList : List Type -> Type where
>   Nil  : HList Nil
>   (::) : {t : Type} -> {ts : List Type} -> t -> HList ts -> HList (t :: ts) 

> head : {t : Type} -> {ts : List Type} -> HList (t :: ts) -> t
> head {t} {ts} (x :: xs) = x

> tail : {t : Type} -> {ts : List Type} -> HList (t :: ts) -> HList ts
> tail {t} {ts} (x :: xs) = xs

> listProd : {ts : List Type} -> HList (map List ts) -> List (HList ts)
> listProd {ts = Nil}        _    = [Nil]
> listProd {ts = (t :: ts')} yzss = [x :: yzs | x <- (head yzss), yzs <- (listProd (tail yzss))]

fails to type check with

- + Errors (1)
 `-- ./HList/UniverseIssue1.lidr line 11 col 7:
     Universe inconsistency.
             Working on: ./HList/UniverseIssue1.lidr.p3
             Old domain: (5,5)
             New domain: (5,4)
             Involved constraints: 
                     ConstraintFC {uconstraint = ./HList/UniverseIssue1.lidr.p3 <= ./HList/UniverseIssue1.lidr.u, ufc = ./HList/UniverseIssue1.lidr:11:8}
                     ConstraintFC {uconstraint = ./HList/UniverseIssue1.lidr.p3 <= ./HList/UniverseIssue1.lidr.u, ufc = ./HList/UniverseIssue1.lidr:11:8}
                     ConstraintFC {uconstraint = ./HList/UniverseIssue1.lidr.s6 <= ./HList/UniverseIssue1.lidr.p3, ufc = ./HList/UniverseIssue1.lidr:19:37-96}

Any idea of what is going on here? Thanks, Nicola