New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ambiguous module qualifier in refined type in imported module induces GHC panic #575

Open
Gabriel439 opened this Issue Jan 14, 2016 · 4 comments

Comments

Projects
None yet
5 participants
@Gabriel439
Copy link
Contributor

Gabriel439 commented Jan 14, 2016

The following module has an ambiguous reference in the refined type for Vector.slice:

module Test where

import Data.Vector (Vector)

import qualified Data.Vector
import qualified Data.Vector         as Vector
import qualified Data.Vector.Mutable as Vector

{-@
assume Vector.slice
    :: n : { n : Int | 0 <= n }
    -> l : { l : Int | 0 <= l }
    -> i : { i : Vector.Vector a | n + l <= len i }
    -> { o : Vector.Vector a | len o = l }
@-}

{-@
example
    :: n : { n : Int | 0 <= n }
    -> l : { l : Int | 0 <= l }
    -> i : { i : Vector.Vector a | n + l <= len i }
    -> { o : Vector.Vector a | len o = l }
@-}
example :: Int -> Int -> Vector a -> Vector a
example = Data.Vector.slice

However, the refinement still succeeds and the above module type-checks. Vector.slice is ambiguous because it could refer to either Data.Vector.slice or Data.Vector.Mutable.slice, although only one of them has the correct type to refine to the given type. Perhaps Liquid Haskell infers which one to refine that way.

However, if you import the above module from another module, like this:

module Test2 where

import Test

... then you get a ghc panic if you type-check the Test2 module:

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

liquid: liquid: panic! (the 'impossible' happened)
  (GHC version 7.10.2 for x86_64-unknown-linux):
    lookupRdrNameInModule

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

If you fix the reference to be unambiguous, like this:

module Test where

import Data.Vector (Vector)

import qualified Data.Vector
import qualified Data.Vector         as Vector
import qualified Data.Vector.Mutable as Vector2

{-@
assume Vector.slice
    :: n : { n : Int | 0 <= n }
    -> l : { l : Int | 0 <= l }
    -> i : { i : Vector.Vector a | n + l <= len i }
    -> { o : Vector.Vector a | len o = l }
@-}

{-@
example
    :: n : { n : Int | 0 <= n }
    -> l : { l : Int | 0 <= l }
    -> i : { i : Vector.Vector a | n + l <= len i }
    -> { o : Vector.Vector a | len o = l }
@-}
example :: Int -> Int -> Vector a -> Vector a
example = Data.Vector.slice

... then the problem disappears.

@nikivazou

This comment has been minimized.

Copy link
Member

nikivazou commented Jan 14, 2016

Thanks for the report and the solution @Gabriel439!

@spinda can you add a check on Bare that rejects the first program with a nice error message?

@gridaphobe

This comment has been minimized.

Copy link
Contributor

gridaphobe commented Jan 15, 2016

@spinda this is probably the offending line:

https://github.com/ucsd-progsys/liquidhaskell/blob/master/src/Language/Haskell/Liquid/Bare/Lookup.hs#L82

We choose the first of multiple matches, when we should in fact throw an error due to the ambiguity.

@spinda spinda self-assigned this Mar 7, 2016

@spinda

This comment has been minimized.

Copy link
Member

spinda commented Mar 7, 2016

All this needs is to throw an error if multiple matches are detected, right?

@ranjitjhala

This comment has been minimized.

Copy link
Member

ranjitjhala commented Mar 7, 2016

yup!

On Sun, Mar 6, 2016 at 10:49 PM, Michael Smith notifications@github.com
wrote:

All this needs is to throw an error if multiple matches are detected,
right?


Reply to this email directly or view it on GitHub
#575 (comment)
.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment