Andreas Abel

> There, the suggested workaround for stack to get just type-checking is: `stack ghci "--ghci-options=-e 1"`. I tried ``` $ stack ghci --main-is Agda:exe:agda --ghci-options='-e 1' ``` but it does...

Ah indeed, after `stack build --dependencies-only` your command "succeeds" (in the sense that it type-checks all modules) and it is as fast the `cabal` version of it. @asr: Do you...

@asr: Did you get a chance to work on this?

> Also, I do not understand why the function is considered projection-like when the type of the first visible argument is `C a`, but not when it is `a`. Why...

I think the problem is that we ever only append more highlighting info to `stSyntaxInfo`, we never reset this state component to empty.

@gallais : Do you have an idea where this behavior could come from?

Maybe another clue: Loading a file with existing agdai in emacs does not activate any highlighting but the deadcode one:

> how often the string `1234567890123456789012345678901234567890` appears in the generated Haskell code, though I'm not sure how to do that. ```sh [ "x$(grep --count -e 1234567890123456789012345678901234567890 Issue7450.hs)" == "x1" ]...

Does `documentation: False` in the `cabal.project` file work, @arybczak ?

ATTN: @emilypi