Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7588 below:

__IMPOSSIBLE__, called at src/full/Agda/Compiler/JS/Compiler.hs:596:45 · Issue #7588 · agda/agda · GitHub

This Agda code crashes the JS backend:

data Cell : Set where
  [-] [o] [x] : Cell

data Board : Set where
  mk-Board : Cell → Cell → Board

winner : Board → Cell
winner = λ where
  (mk-Board [x] [x]) → [x]
  (mk-Board  _  [x]) → [x]
  (mk-Board  _   _ ) → [-]

step : Board → Board
step b with winner b  
... | [-] = b
... |  _  = mk-Board [-] [-]

Here is a log:

/tmp/tmp.4DeC6lEc31$ agda --js bugreport.agda
Checking bugreport (/tmp/tmp.4DeC6lEc31/bugreport.agda).
Compiling Agda.Primitive in /nix/store/8pqr8xp07v8xd4kj99wpkziq5zd2famd-Agda-2.8.0-data/share/ghc-9.6.5/x86_64-linux-ghc-9.6.5/Agda-2.8.0/lib/prim/_build/2.8.0/agda/Agda/Primitive.agdai to /tmp/tmp.4DeC6lEc31/./jAgda.Agda.Primitive.js
Compiling bugreport in /tmp/tmp.4DeC6lEc31/bugreport.agdai to /tmp/tmp.4DeC6lEc31/./jAgda.bugreport.js
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Compiler/JS/Compiler.hs:588:45 in Agda-2.8.0-JMDOmoIw0FQAlAv1YIAPME:Agda.Compiler.JS.Compiler

I get an __IMPOSSIBLE__ error on these Agda revisions:

• df1a26d: Agda 2.7.0

The example compiles without errors on these Agda revisions:

• b499d12: Agda 2.6.3
• 3356568: current tip of primFloatRound broken in JS #7573
• 3425ed5: recent master

The error disappears after any of these edits:

• Delete the [o] constructor
• Delete the 1nd case of winner
• Delete the 2nd case of winner
• Replace λ where with a top-level pattern match
• Delete the 1st with-clause of step
• Replace the 2nd RHS of step with b

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4