Issues with type inference for annotated list literals

[sjakobi]

1. It's redundant to check the kind of the type parameter starting in line 606. Type-inference for List already covers this.

   dhall-haskell/dhall/src/Dhall/TypeCheck.hs

   Lines 597 to 613 in d6d3943

   	ListLit (Just _T₀) ts -> do
   	_ <- loop ctx _T₀
   	let _T₀' = eval values _T₀
   	let _T₀'' = quote names _T₀'
   	case _T₀' of
   	VList _T₁' -> do
   	tT₁' <- loop ctx (quote names _T₁')
   	case tT₁' of
   	VConst Type -> return ()
   	_ -> die (InvalidListType _T₀'')
   	_ -> do
   	die (InvalidListType _T₀'')

2. The subsequent check of the list elements is both wrong and apparently dead code, according to coverage reports. We're trying to compare the type of an element with the full List X annotation. If these were equivalent, the list would actually by ill-typed!

dhall-haskell/dhall/src/Dhall/TypeCheck.hs

Lines 615 to 624 in d6d3943

	let process i t = do
	_T₁' <- loop ctx t
	if Eval.conv values _T₀' _T₁'
	then return ()
	else do
	let _T₁'' = quote names _T₁'
	die (InvalidListElement i _T₀'' t _T₁'')
	traverseWithIndex_ process ts

I think it would be best to completely get rid of the element processing here, but I'm not sure what would be the best way…

A) Pattern match for ListLit (Just _) [] and throw a BrokenInvariant error.
B) Redefine the ListLit constructor to contain a Either (Expr s a) (NonEmptySeq (Expr s a))
C) Make separate constructors for empty and non-empty lists.

[Gabriella439]

@sjakobi: I think the right way to do this is to make separate constructors for empty and non-empty lists

[sjakobi]

I think creating separate constructors might be a slightly larger undertaking than I initially thought. In particular, we'd want (need?!) a data type for non-empty sequences:

• The nonempty-containers package contains a NESeq variant of Seq that would fit the bill nicely. The problem is that nonempty-containers currently requires base >= 4.9 (i.e. GHC >= 8.0) and containers >= 5.9. I suspect that that support for GHC-7.10 could be added, but it seems like quite a bit of work and additional maintenance burden. The situation is probably similar with support for containers-5.6. The maintainer is a Dhall user though, which might facilitate support requests…

• There's another package offering a NonEmptySeq, that would be compatible, but it's much less polished and lacks some functionality, most notably mapWithIndex and reverse.

Ultimately I wonder whether we're still committed to supporting GHC-7.10, even though Eta's future seems increasingly uncertain.

[Gabriella439]

In that case, maybe just add the BrokenInvariant assertion for now

[sjakobi]

I've updated #1359 to add a ListLitInvariant type error.