Fix a corner case for join on 0-length inner sequences.

Both the standard and the reference interpreter were producing
incorrect behaviors.  The correct behavior is to return an
empty sequence.

Fixes #395.

src/Cryptol/Eval/Reference.lhs

@@ -532,11 +532,13 @@ Cryptol primitives fall into several groups:
 >                     VList (fromVList l ++ fromVList r))
 >
 >   , ("join"       , VNumPoly $ \_parts ->
->                     VNumPoly $ \_each  ->
+>                     VNumPoly $ \each  ->
 >                     VPoly $ \_a ->
 >                     VFun $ \xss ->
->                     VList (concat (map fromVList (fromVList xss))))
->     -- FIXME: this doesn't handle the case [inf][0] -> [0]
+>                       case each of
+>                         -- special case when the inner sequences are of length 0
+>                         Nat 0 -> VList []
+>                         _ -> VList (concat (map fromVList (fromVList xss))))
 >
 >   , ("split"      , VNumPoly $ \parts ->
 >                     vFinPoly $ \each  ->

src/Cryptol/Prims/Eval.hs

@@ -582,6 +582,10 @@ joinSeq :: BitWord b w
         -> SeqMap b w
         -> Eval (GenValue b w)
 
+-- Special case for 0 length inner sequences.
+joinSeq _parts 0 a _xs
+  = return $ zeroV (TVSeq 0 a)
+
 -- finite sequence of words
 joinSeq (Nat parts) each TVBit xs
   = joinWords parts each xs

tests/issues/issue395.icry

@@ -0,0 +1,21 @@
+:t (join (zero : [inf][0]))
+join (zero : [inf][0])
+join (zero : [inf][0]) == []
+:eval join (zero : [inf][0])
+
+:t (join (zero : [1000][0]))
+join (zero : [1000][0])
+join (zero : [1000][0]) == []
+:eval join (zero : [1000][0])
+:pro (\(x:[1000][0]) -> join x == [])
+
+:t (join (zero : [inf][0][32]))
+join (zero : [inf][0][32])
+join (zero : [inf][0][32]) == []
+:eval join (zero : [inf][0][32])
+
+:t (join (zero : [1000][0][32]))
+join (zero : [1000][0][32])
+join (zero : [1000][0][32]) == []
+:eval join (zero : [1000][0][32])
+:pro (\(x:[1000][0][32]) -> join x == [])

tests/issues/issue395.icry.stdout

@@ -0,0 +1,19 @@
+Loading module Cryptol
+(join (zero : [inf][0])) : [0]
+0x0
+True
+[]
+(join (zero : [1000][0])) : [0]
+0x0
+True
+[]
+Q.E.D.
+(join (zero : [inf][0][32])) : [0][32]
+[]
+True
+[]
+(join (zero : [1000][0][32])) : [0][32]
+[]
+True
+[]
+Q.E.D.