Skip to content

Records not importing properly in Haskell generated code #454

@SamHarS

Description

@SamHarS

When importing from a file that has a record, the Haskell translation of it fails to compile due to the import only importing the data and not also the record.

Agda code:
File 1:

module Test1 where

record Example (a : Set) : Set where
  no-eta-equality
  field
    f : a  a
open Example public
{-# COMPILE AGDA2HS Example #-}

File 2:

module Test2 where
open import Test1

fExample : {a : Set}  a  a
fExample a = a
{-# COMPILE AGDA2HS fExample #-}

example2 : (a : Set)  Example a
example2 a = record { f = fExample }
{-# COMPILE AGDA2HS example2 #-}

Haskell code:
File 1:

module Test1 where

data Example a = Example{f :: a -> a}

File 2:

module Test2 where

import Test1 (Example)

fExample :: a -> a
fExample a = a

example2 :: Example a
example2 = Example fExample

Error in GHCI:

test2.hs:9:12: error: [GHC-31891]
    * Illegal term-level use of the type constructor or class `Example'
    * imported from `Test1' at test2.hs:3:15-21
      (and originally defined at Test1.hs:3:1-37)
    * Perhaps use one of these:
        variable `fExample' (line 6), variable `example2' (line 9)
      Perhaps you want to add `Example' to the import list
      in the import of `Test1' (test2.hs:3:1-22).
    * In the expression: Example fExample
      In an equation for `example2': example2 = Example fExample
  |
9 | example2 = Example fExample
  |            ^^^^^^^

@martinescardo

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions