search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 134 forks source link

Liquid Haskell gives unusual error message for duplicate INLINE annotaitons #637

Open Gabriella439 opened 8 years ago

Gabriella439 commented 8 years ago

If I type-check the following module with Liquid Haskell:

foo :: ()
foo = ()
{-# INLINE foo #-}

bar :: ()
bar = ()
{-# INLINE foo #-}

... then I get the following error message:

$ stack exec liquid inline.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Cleaned Files ******************************************************

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  Loaded Targets *****************************************************

liquid: Cannot add module Main to context: not a home module

A better error message would help narrow down the problem more quickly

ranjitjhala commented 8 years ago

Whoa! Never seen that before -- probably tickles some dark corner of the GHC API. Will look into ASAP thanks!

gridaphobe commented 8 years ago

That is indeed a GHC error. I believe the issue is that GHC rejects your program because it contains a duplicate INLINE pragma. Usually when this happens we print out GHC's error message, but somehow in this case we're ignoring GHC and trying to add the module to our interactive context anyway.

TL;DR your module is bad, but we need to extract GHC's error message so you can have a hope of fixing it.