GitLab

I have this code

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}


import           Data.Type.Equality ((:~:)(Refl))
import           GHC.TypeLits
import qualified Numeric.LinearAlgebra as LA
import           Numeric.LinearAlgebra.Static


toVec :: forall n . (KnownNat n) => LA.Vector Double -> R n
toVec vec = withVector vec $ \(v :: R n2) -> case sameNat (Proxy @n) (Proxy @n2) of
  Just Refl -> v
  Nothing -> error "wrong dimensions"

Notably I forgot to import Proxy.

Without -fdefer-type-errors I get this error:

➤ nix-shell -p "haskellPackages.ghcWithPackages (pkgs:[pkgs.hmatrix])" --pure --run 'ghci ghc-8.0.2-proxy-confusing-error.hs'
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( ghc-8.0.2-proxy-confusing-error.hs, interpreted )

ghc-8.0.2-proxy-confusing-error.hs:12:60: error:
    Data constructor not in scope: Proxy

ghc-8.0.2-proxy-confusing-error.hs:12:60: error:
    * Cannot apply expression of type `t1'
      to a visible type argument `n'
    * In the first argument of `sameNat', namely `(Proxy @n)'
      In the expression: sameNat (Proxy @n) (Proxy @n2)
      In the expression:
        case sameNat (Proxy @n) (Proxy @n2) of {
          Just Refl -> v
          Nothing -> error "wrong dimensions" }
Failed, modules loaded: none.

but with -fdefer-type-errors the Data constructor not in scope: Proxy is gone!

➤ nix-shell -p "haskellPackages.ghcWithPackages (pkgs:[pkgs.hmatrix])" --pure --run 'ghci ghc-8.0.2-proxy-confusing-error.hs -fdefer-type-errors'
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( ghc-8.0.2-proxy-confusing-error.hs, interpreted )

ghc-8.0.2-proxy-confusing-error.hs:12:60: error:
    * Cannot apply expression of type `t1'
      to a visible type argument `n'
    * In the first argument of `sameNat', namely `(Proxy @n)'
      In the expression: sameNat (Proxy @n) (Proxy @n2)
      In the expression:
        case sameNat (Proxy @n) (Proxy @n2) of {
          Just Refl -> v
          Nothing -> error "wrong dimensions" }
Failed, modules loaded: none.

This is probably related to #12529 (closed).

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	nh2
Operating system
Architecture