gistfile1.txt

Type checking ./Parallax/ByteString/Core.idr
./Parallax/ByteString/Core.idr:32:56:When elaborating right hand side of Parallax.ByteString.Core.case block in case block in case block in case block in case block in case block in peekBits8:
When elaborating argument val to constructor Delay:
        INTERNAL ERROR: Not a guess ? {letty185} : Type 0. let succ' : {letty185} = ?defer Parallax.ByteString.Core.here : (t : Type h15) -> Type j15 -> Parallax.ByteString.Buffer.Buffer -> Parallax.ByteString.Buffer.Buffer -> Prelude.Nat.Nat -> Parallax.Types.Pos -> Parallax.Types.More -> Parallax.Types.More -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> ({letty185} : Type 0) -> {letty185}. Parallax.ByteString.Core.here t {lamp0} buf {lamp1} pos_ {lamp2} more {lamp3} f {lamp4} succ {lamp5} {letty185} in ?defer Parallax.ByteString.Core.ass : (t : Type h15) -> Type j15 -> Parallax.ByteString.Buffer.Buffer -> Parallax.ByteString.Buffer.Buffer -> Prelude.Nat.Nat -> Parallax.Types.Pos -> Parallax.Types.More -> Parallax.Types.More -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> ({letty185} : Type 0) -> {letty185} -> Parallax.Types.IResult String t. Parallax.ByteString.Core.ass t {lamp0} buf {lamp1} pos_ {lamp2} more {lamp3} f {lamp4} succ {lamp5} {letty185} succ'
([{letty185},{val583},{e554},{val550},{e517},{hole12},{hole11},{hole10},{hole9},{hole8},{hole7},{hole6},{hole5},{hole4},{hole3},{hole2},{hole1},{hole0}],?? {hole0} : pty t : Type h15. pty {lamp0} : Type j15. pty buf : Parallax.ByteString.Buffer.Buffer. pty {lamp1} : Parallax.ByteString.Buffer.Buffer. pty pos_ : Prelude.Nat.Nat. pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat t : Type h15. ?? {hole1} : pty {lamp0} : Type j15. pty buf : Parallax.ByteString.Buffer.Buffer. pty {lamp1} : Parallax.ByteString.Buffer.Buffer. pty pos_ : Prelude.Nat.Nat. pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp0} : Type j15. ?? {hole2} : pty buf : Parallax.ByteString.Buffer.Buffer. pty {lamp1} : Parallax.ByteString.Buffer.Buffer. pty pos_ : Prelude.Nat.Nat. pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat buf : Parallax.ByteString.Buffer.Buffer. ?? {hole3} : pty {lamp1} : Parallax.ByteString.Buffer.Buffer. pty pos_ : Prelude.Nat.Nat. pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp1} : Parallax.ByteString.Buffer.Buffer. ?? {hole4} : pty pos_ : Prelude.Nat.Nat. pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat pos_ : Prelude.Nat.Nat. ?? {hole5} : pty {lamp2} : Parallax.Types.Pos. pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp2} : Parallax.Types.Pos. ?? {hole6} : pty more : Parallax.Types.More. pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat more : Parallax.Types.More. ?? {hole7} : pty {lamp3} : Parallax.Types.More. pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp3} : Parallax.Types.More. ?? {hole8} : pty f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat f : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. ?? {hole9} : pty {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp4} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t. ?? {hole10} : pty succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat succ : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. ?? {hole11} : pty {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. Parallax.Types.IResult String t = pat {lamp5} : Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t. ?? {val583} : Parallax.Types.IResult String t = ? {letty185} : Type 0. let succ' : {letty185} = ?defer Parallax.ByteString.Core.here : (t : Type h15) -> Type j15 -> Parallax.ByteString.Buffer.Buffer -> Parallax.ByteString.Buffer.Buffer -> Prelude.Nat.Nat -> Parallax.Types.Pos -> Parallax.Types.More -> Parallax.Types.More -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> ({letty185} : Type 0) -> {letty185}. Parallax.ByteString.Core.here t {lamp0} buf {lamp1} pos_ {lamp2} more {lamp3} f {lamp4} succ {lamp5} {letty185} in ?defer Parallax.ByteString.Core.ass : (t : Type h15) -> Type j15 -> Parallax.ByteString.Buffer.Buffer -> Parallax.ByteString.Buffer.Buffer -> Prelude.Nat.Nat -> Parallax.Types.Pos -> Parallax.Types.More -> Parallax.Types.More -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.List.List String -> String -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> (Parallax.ByteString.Buffer.Buffer -> Parallax.Types.Pos -> Parallax.Types.More -> Prelude.Maybe.Maybe Bits8 -> Parallax.Types.IResult String t) -> ({letty185} : Type 0) -> {letty185} -> Parallax.Types.IResult String t. Parallax.ByteString.Core.ass t {lamp0} buf {lamp1} pos_ {lamp2} more {lamp3} f {lamp4} succ {lamp5} {letty185} succ' in ?? {e554} : Lazy (Parallax.Types.IResult String t) = Delay LazyEval (Parallax.Types.IResult String t) {val583} in ?? {val550} : Parallax.Types.IResult String t = Prelude.Bool.boolElim (Parallax.Types.IResult String t) (Prelude.Classes.== Parallax.Types.More More instance of Prelude.Classes.Eq more Parallax.Types.Complete) (Delay LazyEval (Parallax.Types.IResult String t) (succ buf (Parallax.Types.MkPos pos_) more (Prelude.Maybe.Nothing Bits8))) {e554} in ?? {e517} : Lazy (Parallax.Types.IResult String t) = Delay LazyEval (Parallax.Types.IResult String t) {val550} in ?? {hole12} : Parallax.Types.IResult String t = Prelude.Bool.boolElim (Parallax.Types.IResult String t) (Prelude.Classes.< Prelude.Nat.Nat Nat instance of Prelude.Classes.Ord pos_ (Parallax.ByteString.Buffer.Buffer.length buf)) (Delay LazyEval (Parallax.Types.IResult String t) (succ buf (Parallax.Types.MkPos pos_) more (Prelude.Maybe.Just Bits8 (Parallax.ByteString.Buffer.Buffer.unsafeIndex buf pos_)))) {e517} in {hole12} in {hole11} in {hole10} in {hole9} in {hole8} in {hole7} in {hole6} in {hole5} in {hole4} in {hole3} in {hole2} in {hole1} in {hole0})
        This is probably a bug, or a missing error message.
        Please consider reporting at https://github.com/idris-lang/Idris-dev/issues